1 /-
2 Copyright (c) 2019 Sébastien Gouëzel. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Sébastien Gouëzel
5 -/
6
7 import analysis.calculus.fderiv
src └──────────────────────┘
8
9 /-!
10 # Higher differentiability
11
12 A function is `C^1` on a domain if it is differentiable there, and its derivative is continuous.
13 By induction, it is `C^n` if it is `C^{n-1}` and its (n-1)-th derivative is `C^1` there or,
14 equivalently, if it is `C^1` and its derivative is `C^{n-1}`.
15 Finally, it is `C^∞` if it is `C^n` for all n.
16
17 We formalize these notions by defining iteratively the n-th derivative of a function at the
18 (n-1)-th derivative of the derivative. It is called `iterated_fderiv 𝕜 n f x` where `𝕜` is the
19 field, `n` is the number of iterations, `f` is the function and `x` is the point. We also define a
20 version `iterated_fderiv_within` relative to a domain, as well as predicates `times_cont_diff 𝕜 n f`
21 and `times_cont_diff_on 𝕜 n f s` saying that the function is `C^n`, respectively in the whole space
22 or on the set `s`.
23
24 We prove basic properties of these notions.
25
26 ## Implementation notes
27
28 The n-th derivative of a function belongs to the space E →L[𝕜] (E →L[𝕜] (E ... F)...))),
29 where there are n iterations of `E →L[𝕜]`. We define this space inductively, call it
30 `iterated_continuous_linear_map 𝕜 n E F`, and denote it by `E [×n]→L[𝕜] F`. We can define
31 it inductively either from the left (i.e., saying that the
32 (n+1)-th space S_{n+1} is E →L[𝕜] S_n) or from the right (i.e., saying that
33 the (n+1)-th space associated to F, denoted by S_{n+1} (F), is equal to S_n (E →L[𝕜] F)).
34 For proofs, it turns out to be more convenient to use the latter approach (from the right),
35 as it means to prove things at the (n+1)-th step we only need to understand well enough the
36 derivative in E →L[𝕜] F (contrary to the approach from the left, where one would need to know
37 enough on the n-th derivative to deduce things on the (n+1)-th derivative).
38 In other words, one could define the (n+1)-th derivative either as the derivative of the n-th
39 derivative, or as the n-th derivative of the derivative. We use the latter definition.
40
41 A difficulty is related to universes: the first and second spaces in the sequence, for n=0
42 and 1, are F and E →L[𝕜] F. If E has universe u and F has universe v, then the first one lives in
43 v and the second one in max v u. Since they should live in the same universe (as all the other
44 spaces in the construction), it means that at the 0-th step we should not use F, but ulift it to
45 universe max v u. But we should also ulift its vector space structure and its normed space
46 structure. This can certainly be done, but I decided it was not worth it for now. Therefore, the
47 definition is only made when E and F live in the same universe.
48
49 Regarding the definition of `C^n` functions, there are two equivalent definitions:
50 * require by induction that the function is differentiable, and that its derivative is C^{n-1}
51 * or require that, for all m ≤ n, the m-th derivative is continuous, and for all m < n the m-th
52 derivative is differentiable.
53 The first definition is more efficient for many proofs by induction. The second definition is more
54 satisfactory as it gives concrete information about the n-th derivative (contrary to the first point
55 of view), and moreover it also makes sense for n = ∞.
56
57 Therefore, we give (and use) both definitions, named respectively `times_cont_diff_rec` and
58 `times_cont_diff` (as well as relativized versions on a set). We show that they are equivalent.
59 The first one is mainly auxiliary: in applications, one should always use `times_cont_diff`
60 (but the proofs below use heavily the equivalence to show that `times_cont_diff` is well behaved).
61
62 ## Tags
63
64 derivative, differentiability, higher derivative, C^n
65
66 -/
67
68 noncomputable theory
69 local attribute [instance, priority 10] classical.decidable_inhabited classical.prop_decidable
id └───────────────────────────┘ └──────────────────────┘
src └───────────────────────────┘ └──────────────────────┘
typ └───────────────────────────┘ └──────────────────────┘
70
71 universes u v w
72
73 open set
74 open_locale topological_space
75
76 variables {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
id └──────────────────────┘
src └──────────────────────┘
typ └──────────────────────┘
doc └──────────────────────┘
77 {E : Type u} [normed_group E] [normed_space 𝕜 E]
id └──────────┘ └──────────┘
src └──────────┘ └──────────┘
typ └──────────┘ └──────────┘
doc └──────────┘ └──────────┘
78 {F : Type u} [normed_group F] [normed_space 𝕜 F]
id └──────────┘ └──────────┘
src └──────────┘ └──────────┘
typ └──────────┘ └──────────┘
doc └──────────┘ └──────────┘
79 {G : Type u} [normed_group G] [normed_space 𝕜 G]
id └──────────┘ └──────────┘
src └──────────┘ └──────────┘
typ └──────────┘ └──────────┘
doc └──────────┘ └──────────┘
80 {s s₁ u : set E} {f f₁ : E → F} {f' f₁' : E →L[𝕜] F} {f₂ : E → G}
id └─┘ └─┘ ┴
src └─┘ └─┘ ┴
typ └─┘ └─┘ ┴
doc └─┘ ┴
81 {f₂' : E →L[𝕜] G} {g : F → G} {x : E} {c : F}
id └─┘ ┴
src └─┘ ┴
typ └─┘ ┴
doc └─┘ ┴
82 {L : filter E} {t : set F} {b : E × F → G} {sb : set (E × F)} {p : E × F}
id └────┘ └─┘ ┴ └─┘ ┴ ┴
src └────┘ └─┘ ┴ └─┘ ┴ ┴
typ └────┘ └─┘ ┴ └─┘ ┴ ┴
83 {n : ℕ}
id ┴
src ┴
typ ┴
84
85 include 𝕜
86
87 /--
88 The space `iterated_continuous_linear_map 𝕜 n E F` is the space E →L[𝕜] (E →L[𝕜] (E ... F)...))),
89 defined inductively over `n`. This is the space to which the `n`-th derivative of a function
90 naturally belongs. It is only defined when `E` and `F` live in the same universe.
91 -/
92 def iterated_continuous_linear_map (𝕜 : Type w) [nondiscrete_normed_field 𝕜] :
id └──────────────────────┘ ┴
src └──────────────────────┘
typ └──────────────────────┘ ┴
doc └──────────────────────┘
93 Π (n : ℕ) (E : Type u) [gE : normed_group E] [@normed_space 𝕜 E _ gE]
id ┴ ┴ └──┘ └──────────┘ ┴ └──────────┘ ┴ ┴ └┘
src ┴ └──────────┘ └──────────┘
typ ┴ ┴ └──┘ └──────────┘ ┴ └──────────┘ ┴ ┴ └┘
doc └──────────┘ └──────────┘
94 (F : Type u) [gF : normed_group F] [@normed_space 𝕜 F _ gF], Type u
id └──┘ └──────────┘ ┴ └──────────┘ ┴ ┴ └┘
src └──────────┘ └──────────┘
typ └──┘ └──────────┘ ┴ └──────────┘ ┴ ┴ └┘
doc └──────────┘ └──────────┘
95 | 0 E _ _ F _ _ := F
id ┴
typ ┴
96 | (n+1) E _ _ F _ _ := by { resetI, exact iterated_continuous_linear_map n E (E →L[𝕜] F) }
id ┴ └────────────────────────────┘ ┴ ┴ └─┘┴┴ ┴
src ┴ └────┘ └────┘ ┴ ┴ ┴ ┴└─┘ ┴┴ └┘
typ ┴ └────┘ └────┘└────────────────────────────┘┴┴┴ ┴ ┴┴└─┘┴┴┴┴└┘
doc └────┘ └────┘ ┴ ┴ ┴ ┴└─┘ ┴┴ └┘
txt └────┘ └────┘ ┴ ┴ ┴ ┴ ┴ └┘
par └────┘ └────┘ ┴ ┴ ┴ ┴ ┴ └┘
pid ┴ ┴ ┴ ┴ ┴ ┴ ┴┴
st └──────────────────────────────────────────────────────────────┘└┘
97
98 notation E `[×`:25 n `]→L[`:25 𝕜 `] ` F := iterated_continuous_linear_map 𝕜 n E F
id └────────────────────────────┘
src └────────────────────────────┘
typ └────────────────────────────┘
doc └────────────────────────────┘
99
100 /--
101 Define by induction a normed group structure on the space of iterated continuous linear
102 maps. To avoid `resetI` in the statement, use the @ version with all parameters. As the equation
103 compiler chokes on this one, we use the `nat.rec_on` version.
104 -/
105 def iterated_continuous_linear_map.normed_group_rec (𝕜 : Type w) [h𝕜 : nondiscrete_normed_field 𝕜]
id └──────────────────────┘ ┴
src └──────────────────────┘
typ └──────────────────────┘ ┴
doc └──────────────────────┘
106 (n : ℕ) (E : Type u) [gE : normed_group E] [sE : normed_space 𝕜 E] :
id ┴ └──────────┘ ┴ └──────────┘ ┴ ┴
src ┴ └──────────┘ └──────────┘
typ ┴ └──────────┘ ┴ └──────────┘ ┴ ┴
doc └──────────┘ └──────────┘
107 ∀(F : Type u) [nF : normed_group F] [sF : @normed_space 𝕜 F _ nF],
id └──┘ └──────────┘ ┴ └──────────┘ ┴ ┴ └┘
src └──────────┘ └──────────┘
typ └──┘ └──────────┘ ┴ └──────────┘ ┴ ┴ └┘
doc └──────────┘ └──────────┘
108 normed_group (@iterated_continuous_linear_map 𝕜 h𝕜 n E gE sE F nF sF) :=
id └──────────┘ └────────────────────────────┘ ┴ └┘ ┴ ┴ └┘ └┘ ┴ └┘ └┘
src └──────────┘ └────────────────────────────┘
typ └──────────┘ └────────────────────────────┘ ┴ └┘ ┴ ┴ └┘ └┘ ┴ └┘ └┘
doc └──────────┘ └────────────────────────────┘
109 nat.rec_on n (λF nF sF, nF) (λn aux_n F nF sF, by { resetI, apply aux_n })
id └────────┘ ┴ ┴ └┘ └┘ └┘ ┴ └───┘ ┴ └┘ └┘
src └────────┘ └────┘ └────┘ ┴
typ └────────┘ ┴ ┴ └┘ └┘ └┘ ┴ └───┘ ┴ └┘ └┘ └────┘ └────┘ ┴
doc └────┘ └────┘ ┴
txt └────┘ └────┘ ┴
par └────┘ └────┘ ┴
pid ┴ ┴
st └─────────────────────┘└┘
110
111 /--
112 Define by induction a normed space structure on the space of iterated continuous linear
113 maps. To avoid `resetI` in the statement, use the @ version with all parameters. As the equation
114 compiler chokes on this one, we use the `nat.rec_on` version.
115 -/
116 def iterated_continuous_linear_map.normed_space_rec (𝕜 : Type w) [h𝕜 : nondiscrete_normed_field 𝕜]
id └──────────────────────┘ ┴
src └──────────────────────┘
typ └──────────────────────┘ ┴
doc └──────────────────────┘
117 (n : ℕ) (E : Type u) [gE : normed_group E] [sE : normed_space 𝕜 E] :
id ┴ └──────────┘ ┴ └──────────┘ ┴ ┴
src ┴ └──────────┘ └──────────┘
typ ┴ └──────────┘ ┴ └──────────┘ ┴ ┴
doc └──────────┘ └──────────┘
118 ∀(F : Type u) [nF : normed_group F] [sF : @normed_space 𝕜 F _ nF],
id └──┘ └──────────┘ ┴ └──────────┘ ┴ ┴ └┘
src └──────────┘ └──────────┘
typ └──┘ └──────────┘ ┴ └──────────┘ ┴ ┴ └┘
doc └──────────┘ └──────────┘
119 @normed_space 𝕜 (@iterated_continuous_linear_map 𝕜 h𝕜 n E gE sE F nF sF)
id └──────────┘ ┴ └────────────────────────────┘ ┴ └┘ ┴ ┴ └┘ └┘ ┴ └┘ └┘
src └──────────┘ └────────────────────────────┘
typ └──────────┘ ┴ └────────────────────────────┘ ┴ └┘ ┴ ┴ └┘ └┘ ┴ └┘ └┘
doc └──────────┘ └────────────────────────────┘
120 _ (@iterated_continuous_linear_map.normed_group_rec 𝕜 h𝕜 n E gE sE F nF sF) :=
id └─────────────────────────────────────────────┘ ┴ └┘ ┴ ┴ └┘ └┘ ┴ └┘ └┘
src └─────────────────────────────────────────────┘
typ └─────────────────────────────────────────────┘ ┴ └┘ ┴ ┴ └┘ └┘ ┴ └┘ └┘
doc └─────────────────────────────────────────────┘
121 nat.rec_on n (λF nF sF, sF) (λn aux_n F nF sF, by { resetI, apply aux_n })
id └────────┘ ┴ ┴ └┘ └┘ └┘ ┴ └───┘ ┴ └┘ └┘
src └────────┘ └────┘ └────┘ ┴
typ └────────┘ ┴ ┴ └┘ └┘ └┘ ┴ └───┘ ┴ └┘ └┘ └────┘ └────┘ ┴
doc └────┘ └────┘ ┴
txt └────┘ └────┘ ┴
par └────┘ └────┘ ┴
pid ┴ ┴
st └─────────────────────┘└┘
122
123 /--
124 Explicit normed group structure on the space of iterated continuous linear maps.
125 -/
126 instance iterated_continuous_linear_map.normed_group (n : ℕ)
id ┴
src ┴
typ ┴
127 (𝕜 : Type w) [h𝕜 : nondiscrete_normed_field 𝕜]
id └──────────────────────┘ ┴
src └──────────────────────┘
typ └──────────────────────┘ ┴
doc └──────────────────────┘
128 (E : Type u) [gE : normed_group E] [sE : normed_space 𝕜 E]
id └──────────┘ ┴ └──────────┘ ┴ ┴
src └──────────┘ └──────────┘
typ └──────────┘ ┴ └──────────┘ ┴ ┴
doc └──────────┘ └──────────┘
129 (F : Type u) [gF : normed_group F] [sF : normed_space 𝕜 F] :
id └──────────┘ ┴ └──────────┘ ┴ ┴
src └──────────┘ └──────────┘
typ └──────────┘ ┴ └──────────┘ ┴ ┴
doc └──────────┘ └──────────┘
130 normed_group (E [×n]→L[𝕜] F) :=
id └──────────┘ ┴ └┘┴└──┘┴┴ ┴
src └──────────┘ └┘ └──┘ ┴
typ └──────────┘ ┴ └┘┴└──┘┴┴ ┴
doc └──────────┘ └┘ └──┘ ┴
131 iterated_continuous_linear_map.normed_group_rec 𝕜 n E F
id └─────────────────────────────────────────────┘ ┴ ┴ ┴ ┴
src └─────────────────────────────────────────────┘
typ └─────────────────────────────────────────────┘ ┴ ┴ ┴ ┴
doc └─────────────────────────────────────────────┘
132
133 instance : inhabited (E [×n]→L[𝕜] F) := ⟨0⟩
id └───────┘ ┴ └┘┴└──┘┴┴ ┴
src └───────┘ └┘ └──┘ ┴
typ └───────┘ ┴ └┘┴└──┘┴┴ ┴
doc └┘ └──┘ ┴
134
135 /--
136 Explicit normed space structure on the space of iterated continuous linear maps.
137 -/
138 instance iterated_continuous_linear_map.normed_space (n : ℕ)
id ┴
src ┴
typ ┴
139 (𝕜 : Type w) [h𝕜 : nondiscrete_normed_field 𝕜]
id └──────────────────────┘ ┴
src └──────────────────────┘
typ └──────────────────────┘ ┴
doc └──────────────────────┘
140 (E : Type u) [gE : normed_group E] [sE : normed_space 𝕜 E]
id └──────────┘ ┴ └──────────┘ ┴ ┴
src └──────────┘ └──────────┘
typ └──────────┘ ┴ └──────────┘ ┴ ┴
doc └──────────┘ └──────────┘
141 (F : Type u) [gF : normed_group F] [sF : normed_space 𝕜 F] :
id └──────────┘ ┴ └──────────┘ ┴ ┴
src └──────────┘ └──────────┘
typ └──────────┘ ┴ └──────────┘ ┴ ┴
doc └──────────┘ └──────────┘
142 normed_space 𝕜 (E [×n]→L[𝕜] F) :=
id └──────────┘ ┴ ┴ └┘┴└──┘┴┴ ┴
src └──────────┘ └┘ └──┘ ┴
typ └──────────┘ ┴ ┴ └┘┴└──┘┴┴ ┴
doc └──────────┘ └┘ └──┘ ┴
143 iterated_continuous_linear_map.normed_space_rec 𝕜 n E F
id └─────────────────────────────────────────────┘ ┴ ┴ ┴ ┴
src └─────────────────────────────────────────────┘
typ └─────────────────────────────────────────────┘ ┴ ┴ ┴ ┴
doc └─────────────────────────────────────────────┘
144
145 /--
146 The n-th derivative of a function, defined inductively by saying that the (n+1)-th
147 derivative of f is the n-th derivative of the derivative of f.
148 -/
149 def iterated_fderiv (𝕜 : Type w) [h𝕜 : nondiscrete_normed_field 𝕜] (n : ℕ)
id └──────────────────────┘ ┴ ┴
src └──────────────────────┘ ┴
typ └──────────────────────┘ ┴ ┴
doc └──────────────────────┘
150 {E : Type u} [gE : normed_group E] [sE : normed_space 𝕜 E] :
id └──────────┘ ┴ └──────────┘ ┴ ┴
src └──────────┘ └──────────┘
typ └──────────┘ ┴ └──────────┘ ┴ ┴
doc └──────────┘ └──────────┘
151 ∀{F : Type u} [gF : normed_group F] [sF : @normed_space 𝕜 F _ gF] (f : E → F),
id └──┘ └──────────┘ ┴ └──────────┘ ┴ ┴ └┘ ┴ ┴ ┴
src └──────────┘ └──────────┘
typ └──┘ └──────────┘ ┴ └──────────┘ ┴ ┴ └┘ ┴ ┴ ┴
doc └──────────┘ └──────────┘
152 E → @iterated_continuous_linear_map 𝕜 h𝕜 n E gE sE F gF sF :=
id ┴ └────────────────────────────┘ ┴ └┘ ┴ ┴ └┘ └┘ ┴ └┘ └┘
src └────────────────────────────┘
typ ┴ └────────────────────────────┘ ┴ └┘ ┴ ┴ └┘ └┘ ┴ └┘ └┘
doc └────────────────────────────┘
153 nat.rec_on n (λF gF sF f, f) (λn rec F gF sF f, by { resetI, exact rec (fderiv 𝕜 f) })
id └────────┘ ┴ ┴ └┘ └┘ ┴ ┴ ┴ └─┘ ┴ └┘ └┘ ┴ └─┘ └────┘ ┴ ┴
src └────────┘ └────┘ └────┘ ┴ └────┘┴ ┴ └┘
typ └────────┘ ┴ ┴ └┘ └┘ ┴ ┴ ┴ └─┘ ┴ └┘ └┘ ┴ └────┘ └────┘└─┘┴ └────┘┴┴┴┴└┘
doc └────┘ └────┘ ┴ └────┘┴ ┴ └┘
txt └────┘ └────┘ ┴ ┴ ┴ └┘
par └────┘ └────┘ ┴ ┴ ┴ └┘
pid ┴ ┴ ┴ ┴ ┴┴
st └────────────────────────────────┘└┘
154
155 @[simp] lemma iterated_fderiv_zero :
doc └──┘
156 iterated_fderiv 𝕜 0 f = f := rfl
id └─────────────┘ ┴ ┴ ┴ ┴ └─┘
src └─────────────┘ ┴ └─┘
typ └─────────────┘ ┴ ┴ ┴ ┴ └─┘
doc └─────────────┘
157
158 @[simp] lemma iterated_fderiv_succ :
doc └──┘
159 iterated_fderiv 𝕜 (n+1) f = (iterated_fderiv 𝕜 n (λx, fderiv 𝕜 f x) : _) := rfl
id └─────────────┘ ┴ ┴┴ ┴ ┴ └─────────────┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ └─┘
src └─────────────┘ ┴ ┴ └─────────────┘ └────┘ └─┘
typ └─────────────┘ ┴ ┴┴ ┴ ┴ └─────────────┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ └─┘
doc └─────────────┘ └─────────────┘ └────┘
160
161 /--
162 The n-th derivative of a function along a set, defined inductively by saying that the (n+1)-th
163 derivative of f is the n-th derivative of the derivative of f.
164 -/
165 def iterated_fderiv_within (𝕜 : Type w) [h𝕜 :nondiscrete_normed_field 𝕜] (n : ℕ)
id └──────────────────────┘ ┴ ┴
src └──────────────────────┘ ┴
typ └──────────────────────┘ ┴ ┴
doc └──────────────────────┘
166 {E : Type u} [gE : normed_group E] [sE : normed_space 𝕜 E] :
id └──────────┘ ┴ └──────────┘ ┴ ┴
src └──────────┘ └──────────┘
typ └──────────┘ ┴ └──────────┘ ┴ ┴
doc └──────────┘ └──────────┘
167 ∀{F : Type u} [gF : normed_group F] [sF : @normed_space 𝕜 F _ gF] (f : E → F) (s : set E),
id └──┘ └──────────┘ ┴ └──────────┘ ┴ ┴ └┘ ┴ ┴ ┴ └─┘ ┴
src └──────────┘ └──────────┘ └─┘
typ └──┘ └──────────┘ ┴ └──────────┘ ┴ ┴ └┘ ┴ ┴ ┴ └─┘ ┴
doc └──────────┘ └──────────┘
168 E → @iterated_continuous_linear_map 𝕜 h𝕜 n E gE sE F gF sF :=
id ┴ └────────────────────────────┘ ┴ └┘ ┴ ┴ └┘ └┘ ┴ └┘ └┘
src └────────────────────────────┘
typ ┴ └────────────────────────────┘ ┴ └┘ ┴ ┴ └┘ └┘ ┴ └┘ └┘
doc └────────────────────────────┘
169 nat.rec_on n (λF gF sF f s, f) (λn rec F gF sF f s, by { resetI, exact rec (fderiv_within 𝕜 f s) s})
id └────────┘ ┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ └┘ └┘ ┴ ┴ └─┘ └───────────┘ ┴ ┴ ┴
src └────────┘ └────┘ └────┘ ┴ └───────────┘┴ ┴ ┴ └┘
typ └────────┘ ┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ └┘ └┘ ┴ ┴ └────┘ └────┘└─┘┴ └───────────┘┴┴┴┴┴ └┘┴
doc └────┘ └────┘ ┴ └───────────┘┴ ┴ ┴ └┘
txt └────┘ └────┘ ┴ ┴ ┴ ┴ └┘
par └────┘ └────┘ ┴ ┴ ┴ ┴ └┘
pid ┴ ┴ ┴ ┴ ┴ └┘
st └──────────────────────────────────────────┘└┘
170
171 @[simp] lemma iterated_fderiv_within_zero :
doc └──┘
172 iterated_fderiv_within 𝕜 0 f s = f := rfl
id └────────────────────┘ ┴ ┴ ┴ ┴ ┴ └─┘
src └────────────────────┘ ┴ └─┘
typ └────────────────────┘ ┴ ┴ ┴ ┴ ┴ └─┘
doc └────────────────────┘
173
174 @[simp] lemma iterated_fderiv_within_succ :
doc └──┘
175 iterated_fderiv_within 𝕜 (n+1) f s
id └────────────────────┘ ┴ ┴┴ ┴ ┴
src └────────────────────┘ ┴
typ └────────────────────┘ ┴ ┴┴ ┴ ┴
doc └────────────────────┘
176 = (iterated_fderiv_within 𝕜 n (λx, fderiv_within 𝕜 f s x) s : _) := rfl
id ┴ └────────────────────┘ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴ └─┘
src ┴ └────────────────────┘ └───────────┘ └─┘
typ ┴ └────────────────────┘ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴ └─┘
doc └────────────────────┘ └───────────┘
177
178 theorem iterated_fderiv_within_univ {n : ℕ} :
id ┴
src ┴
typ ┴
179 iterated_fderiv_within 𝕜 n f univ = iterated_fderiv 𝕜 n f :=
id └────────────────────┘ ┴ ┴ ┴ └──┘ ┴ └─────────────┘ ┴ ┴ ┴
src └────────────────────┘ └──┘ ┴ └─────────────┘
typ └────────────────────┘ ┴ ┴ ┴ └──┘ ┴ └─────────────┘ ┴ ┴ ┴
doc └────────────────────┘ └─────────────┘
180 begin
st └─────
181 tactic.unfreeze_local_instances,
id └─────────────────────────────┘
src └─────────────────────────────┘
typ └─────────────────────────────┘
doc └─────────────────────────────┘
par └─────────────────────────────┘
st ───────────────────────────────────
182 induction n with n IH generalizing F,
id ┴
src └────────┘ └───────────────────────┘
typ └────────┘┴└───────────────────────┘
doc └────────┘ └───────────────────────┘
txt └────────┘ └───────────────────────┘
par └────────┘ └───────────────────────┘
pid ┴ ┴└───────┘└─────────────┘
st ─────────────────────────────────────┘└─
183 { refl },
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st ───┘└───┘└┘└
184 { simp [IH] }
src └────┘ └┘
typ └────┘└┘└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴┴ ┴┴
st ─────────────┘└─
185 end
st ──┘
186
187 /--
188 If two functions coincide on a set `s` of unique differentiability, then their iterated
189 differentials within this set coincide.
190 -/
191 lemma iterated_fderiv_within_congr (hs : unique_diff_on 𝕜 s)
id └────────────┘ ┴ ┴
src └────────────┘
typ └────────────┘ ┴ ┴
doc └────────────┘
192 (hL : ∀y∈s, f₁ y = f y) (hx : x ∈ s) :
id ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
193 iterated_fderiv_within 𝕜 n f₁ s x = iterated_fderiv_within 𝕜 n f s x :=
id └────────────────────┘ ┴ ┴ └┘ ┴ ┴ ┴ └────────────────────┘ ┴ ┴ ┴ ┴ ┴
src └────────────────────┘ ┴ └────────────────────┘
typ └────────────────────┘ ┴ ┴ └┘ ┴ ┴ ┴ └────────────────────┘ ┴ ┴ ┴ ┴ ┴
doc └────────────────────┘ └────────────────────┘
194 begin
st └─────
195 tactic.unfreeze_local_instances,
id └─────────────────────────────┘
src └─────────────────────────────┘
typ └─────────────────────────────┘
doc └─────────────────────────────┘
par └─────────────────────────────┘
st ───────────────────────────────────
196 induction n with n IH generalizing F f x,
id ┴
src └────────┘ └───────────────────────────┘
typ └────────┘┴└───────────────────────────┘
doc └────────┘ └───────────────────────────┘
txt └────────┘ └───────────────────────────┘
par └────────┘ └───────────────────────────┘
pid ┴ ┴└───────┘└─────────────────┘
st ─────────────────────────────────────────┘└─
197 { simp [hL x hx] },
id └┘ ┴ └┘
src └────┘ ┴ ┴ └┘
typ └────┘└┘┴┴┴└┘└┘
doc └────┘ ┴ ┴ └┘
txt └────┘ ┴ ┴ └┘
par └────┘ ┴ ┴ └┘
pid ┴┴ ┴ ┴ ┴┴
st ───┘└─────────────┘└┘└
198 { simp only [iterated_fderiv_within_succ],
id └─────────────────────────┘
src └─────────┘└─────────────────────────┘┴
typ └─────────┘└─────────────────────────┘┴
doc └─────────┘ ┴
txt └─────────┘ ┴
par └─────────┘ ┴
pid ┴└──┘└┘ ┴
st ──────────────────────────────────────────┘└─
199 refine IH (λy hy, _) hx,
id └┘ └┘
src └─────┘ ┴ └───────┘
typ └─────┘└┘┴ └───────┘└┘
doc └─────┘ ┴ └───────┘
txt └─────┘ ┴ └───────┘
par └─────┘ ┴ └───────┘
pid ┴ ┴ └───────┘
st ──────────────────────────┘└─
200 apply fderiv_within_congr (hs y hy) hL (hL y hy) }
id └─────────────────┘ └┘ └┘ ┴ └┘
src └────┘└─────────────────┘┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘
typ └────┘└─────────────────┘┴ └┘┴ ┴ └┘ ┴ └┘┴┴┴└┘└┘
doc └────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘
txt └────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘
par └────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘
pid ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴┴
st ────────────────────────────────────────────────────┘└─
201 end
st ──┘
202
203 /--
204 The iterated differential within a set `s` at a point `x` is not modified if one intersects
205 `s` with an open set containing `x`.
206 -/
207 lemma iterated_fderiv_within_inter_open (xu : x ∈ u) (hu : is_open u) (xs : x ∈ s)
id ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴
src ┴ └─────┘ ┴
typ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴
doc └─────┘
208 (hs : unique_diff_on 𝕜 (s ∩ u)) :
id └────────────┘ ┴ ┴ ┴ ┴
src └────────────┘ ┴
typ └────────────┘ ┴ ┴ ┴ ┴
doc └────────────┘
209 iterated_fderiv_within 𝕜 n f (s ∩ u) x = iterated_fderiv_within 𝕜 n f s x :=
id └────────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────────────────────┘ ┴ ┴ ┴ ┴ ┴
src └────────────────────┘ ┴ ┴ └────────────────────┘
typ └────────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────────────────────┘ ┴ ┴ ┴ ┴ ┴
doc └────────────────────┘ └────────────────────┘
210 begin
st └─────
211 tactic.unfreeze_local_instances,
id └─────────────────────────────┘
src └─────────────────────────────┘
typ └─────────────────────────────┘
doc └─────────────────────────────┘
par └─────────────────────────────┘
st ───────────────────────────────────
212 induction n with n IH generalizing F f,
id ┴
src └────────┘ └─────────────────────────┘
typ └────────┘┴└─────────────────────────┘
doc └────────┘ └─────────────────────────┘
txt └────────┘ └─────────────────────────┘
par └────────┘ └─────────────────────────┘
pid ┴ ┴└───────┘└───────────────┘
st ───────────────────────────────────────┘└─
213 { simp },
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st ───┘└───┘└┘└
214 { simp,
src └──┘
typ └──┘
doc └──┘
txt └──┘
par └──┘
st ───────┘└─
215 rw ← IH,
src └───┘
typ └───┘└┘
doc └───┘
txt └───┘
par └───┘
pid └─┘
st ──────────┘└─
216 apply iterated_fderiv_within_congr hs (λy hy, _) ⟨xs, xu⟩,
id └──────────────────────────┘ └┘ └┘ └┘
src └────┘└──────────────────────────┘┴ ┴ └───────┘ └┘ ┴
typ └────┘└──────────────────────────┘┴└┘┴ └───────┘ └┘└┘└┘┴
doc └────┘└──────────────────────────┘┴ ┴ └───────┘ └┘ ┴
txt └────┘ ┴ ┴ └───────┘ └┘ ┴
par └────┘ ┴ ┴ └───────┘ └┘ ┴
pid ┴ ┴ ┴ └───────┘ └┘ ┴
st ────────────────────────────────────────────────────────────┘└─
217 apply fderiv_within_inter (mem_nhds_sets hu hy.2),
id └─────────────────┘ └───────────┘ └┘ └┘
src └────┘└─────────────────┘┴ └───────────┘┴ ┴ └─┘
typ └────┘└─────────────────┘┴ └───────────┘┴└┘┴└┘└─┘
doc └────┘ ┴ ┴ ┴ └─┘
txt └────┘ ┴ ┴ ┴ └─┘
par └────┘ ┴ ┴ ┴ └─┘
pid ┴ ┴ ┴ ┴ └─┘
st ────────────────────────────────────────────────────┘└─
218 have := hs y hy,
id └┘ ┴ └┘
src └──────┘ ┴ ┴
typ └──────┘└┘┴┴┴└┘
doc └──────┘ ┴ ┴
txt └──────┘ ┴ ┴
par └──────┘ ┴ ┴
pid └───┘└─┘ ┴ ┴
st ──────────────────┘└─
219 rwa unique_diff_within_at_inter (mem_nhds_sets hu hy.2) at this }
id └─────────────────────────┘ └───────────┘ └┘ └┘
src └──┘└─────────────────────────┘┴ └───────────┘┴ ┴ └──────────┘
typ └──┘└─────────────────────────┘┴ └───────────┘┴└┘┴└┘└──────────┘
doc └──┘ ┴ ┴ ┴ └──────────┘
txt └──┘ ┴ ┴ ┴ └──────────┘
par └──┘ ┴ ┴ ┴ └──────────┘
pid ┴ ┴ ┴ ┴ └─┘└──────┘┴
st ───────────────────────────────────────────────────────────────────┘└─
220 end
st ──┘
221
222 /--
223 The iterated differential within a set `s` at a point `x` is not modified if one intersects
224 `s` with a neighborhood of `x`.
225 -/
226 lemma iterated_fderiv_within_inter (hu : u ∈ 𝓝 x) (xs : x ∈ s)
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc ┴
227 (hs : unique_diff_on 𝕜 s) :
id └────────────┘ ┴ ┴
src └────────────┘
typ └────────────┘ ┴ ┴
doc └────────────┘
228 iterated_fderiv_within 𝕜 n f (s ∩ u) x = iterated_fderiv_within 𝕜 n f s x :=
id └────────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────────────────────┘ ┴ ┴ ┴ ┴ ┴
src └────────────────────┘ ┴ ┴ └────────────────────┘
typ └────────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────────────────────┘ ┴ ┴ ┴ ┴ ┴
doc └────────────────────┘ └────────────────────┘
229 begin
st └─────
230 rcases mem_nhds_sets_iff.1 hu with ⟨v, vu, v_open, xv⟩,
id └───────────────┘ └┘
src └─────┘└───────────────┘└─┘ └───────────────────────┘
typ └─────┘└───────────────┘└─┘└┘└───────────────────────┘
doc └─────┘ └─┘ └───────────────────────┘
txt └─────┘ └─┘ └───────────────────────┘
par └─────┘ └─┘ └───────────────────────┘
pid ┴ └─┘ └───────────────────────┘
st ───────────────────────────────────────────────────────┘└─
231 have A : (s ∩ u) ∩ v = s ∩ v,
id ┴ ┴ ┴ ┴ ┴
src └───────┘ ┴┴┴ └┘ ┴ ┴┴┴ ┴ ┴
typ └───────┘ ┴┴┴┴└┘ ┴ ┴┴┴┴┴ ┴┴
doc └───────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴
txt └───────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴
par └───────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴
pid └────┘└─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴
st ─────────────────────────────┘└─
232 { apply subset.antisymm (inter_subset_inter (inter_subset_left _ _) (subset.refl _)),
id └─────────────┘ └────────────────┘ └───────────────┘ └─────────┘
src └────┘└─────────────┘┴ └────────────────┘┴ └───────────────┘└────┘ └─────────┘└──┘
typ └────┘└─────────────┘┴ └────────────────┘┴ └───────────────┘└────┘ └─────────┘└──┘
doc └────┘ ┴ ┴ └────┘ └──┘
txt └────┘ ┴ ┴ └────┘ └──┘
par └────┘ ┴ ┴ └────┘ └──┘
pid ┴ ┴ ┴ └────┘ └──┘
st ───┘└────────────────────────────────────────────────────────────────────────────────┘└─
233 exact λ y ⟨ys, yv⟩, ⟨⟨ys, vu yv⟩, yv⟩ },
id └┘ └┘ └┘
src └────┘ └──┘ └┘ └─┘ └┘ ┴ └─┘ └┘
typ └────┘ └──┘└┘└┘└┘└─┘ └┘└┘┴ └─┘ └┘
doc └────┘ └──┘ └┘ └─┘ └┘ ┴ └─┘ └┘
txt └────┘ └──┘ └┘ └─┘ └┘ ┴ └─┘ └┘
par └────┘ └──┘ └┘ └─┘ └┘ ┴ └─┘ └┘
pid ┴ └──┘ └┘ └─┘ └┘ ┴ └─┘ ┴┴
st ─────────────────────────────────────────┘└┘└
234 have : iterated_fderiv_within 𝕜 n f (s ∩ v) x = iterated_fderiv_within 𝕜 n f s x :=
id ┴ └────────────────────┘ ┴ ┴ ┴ ┴ ┴
src └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴└────────────────────┘┴ ┴ ┴ ┴ ┴ └───
typ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴┴└┘ ┴ ┴└────────────────────┘┴┴┴┴┴┴┴┴┴┴└───
doc └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴└────────────────────┘┴ ┴ ┴ ┴ ┴ └───
txt └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───
par └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───
pid └───┘└┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───
st ──────────────────────────────────────────────────────────────────────────────────────
235 iterated_fderiv_within_inter_open xv v_open xs (hs.inter v_open),
id └───────────────────────────────┘ └┘ └┘ └──────┘ └────┘
src ───┘└───────────────────────────────┘┴ ┴ ┴ ┴ └──────┘┴ ┴
typ ───┘└───────────────────────────────┘┴└┘┴ ┴└┘┴ └──────┘┴└────┘┴
doc ───┘└───────────────────────────────┘┴ ┴ ┴ ┴ ┴ ┴
txt ───┘ ┴ ┴ ┴ ┴ ┴ ┴
par ───┘ ┴ ┴ ┴ ┴ ┴ ┴
pid ───┘ ┴ ┴ ┴ ┴ ┴ ┴
st ───────────────────────────────────────────────────────────────────┘└─
236 rw ← this,
id └──┘
src └───┘
typ └───┘└──┘
doc └───┘
txt └───┘
par └───┘
pid └─┘
st ──────────┘└─
237 have : iterated_fderiv_within 𝕜 n f ((s ∩ u) ∩ v) x = iterated_fderiv_within 𝕜 n f (s ∩ u) x,
id ┴ └────────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴└────────────────────┘┴ ┴ ┴ ┴ ┴ ┴ └┘
typ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴┴└┘ ┴ ┴└────────────────────┘┴┴┴┴┴┴┴ ┴┴ ┴┴└┘┴
doc └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴└────────────────────┘┴ ┴ ┴ ┴ ┴ ┴ └┘
txt └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
par └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
pid └───┘└┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
st ─────────────────────────────────────────────────────────────────────────────────────────────┘└─
238 { refine iterated_fderiv_within_inter_open xv v_open ⟨xs, mem_of_nhds hu⟩ _,
id └───────────────────────────────┘ └┘ └────┘ └┘ └─────────┘ └┘
src └─────┘└───────────────────────────────┘┴ ┴ ┴ └┘└─────────┘┴ └─┘
typ └─────┘└───────────────────────────────┘┴└┘┴└────┘┴ └┘└┘└─────────┘┴└┘└─┘
doc └─────┘└───────────────────────────────┘┴ ┴ ┴ └┘ ┴ └─┘
txt └─────┘ ┴ ┴ ┴ └┘ ┴ └─┘
par └─────┘ ┴ ┴ ┴ └┘ ┴ └─┘
pid ┴ ┴ ┴ ┴ └┘ ┴ └─┘
st ───┘└───────────────────────────────────────────────────────────────────────┘└─
239 rw A,
id ┴
src └─┘
typ └─┘┴
doc └─┘
txt └─┘
par └─┘
pid ┴
st ───────┘└─
240 exact hs.inter v_open },
id └──────┘ └────┘
src └────┘└──────┘┴ ┴
typ └────┘└──────┘┴└────┘┴
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ─────────────────────────┘└┘└
241 rw A at this,
id ┴
src └─┘ └──────┘
typ └─┘┴└──────┘
doc └─┘ └──────┘
txt └─┘ └──────┘
par └─┘ └──────┘
pid ┴ └──────┘
st ─────────────┘└─
242 rw ← this
id └──┘
src └───┘ ┴
typ └───┘└──┘┴
doc └───┘ ┴
txt └───┘ ┴
par └───┘ ┴
pid └─┘ ┴
st ───────────┘
243 end
st └─┘
244
245 /--
246 Auxiliary definition defining `C^n` functions by induction over `n`.
247 In applications, use `times_cont_diff` instead.
248 -/
249 def times_cont_diff_rec (𝕜 : Type w) [nondiscrete_normed_field 𝕜] :
id └──────────────────────┘ ┴
src └──────────────────────┘
typ └──────────────────────┘ ┴
doc └──────────────────────┘
250 Π (n : ℕ) {E : Type u} [gE : normed_group E] [@normed_space 𝕜 E _ gE]
id ┴ ┴ └──┘ └──────────┘ ┴ └──────────┘ ┴ ┴ └┘
src ┴ └──────────┘ └──────────┘
typ ┴ ┴ └──┘ └──────────┘ ┴ └──────────┘ ┴ ┴ └┘
doc └──────────┘ └──────────┘
251 {F : Type u} [gF : normed_group F] [@normed_space 𝕜 F _ gF] (f : E → F), Prop
id └──┘ └──────────┘ ┴ └──────────┘ ┴ ┴ └┘ ┴ ┴ ┴
src └──────────┘ └──────────┘
typ └──┘ └──────────┘ ┴ └──────────┘ ┴ ┴ └┘ ┴ ┴ ┴
doc └──────────┘ └──────────┘
252 | 0 E _ _ F _ _ f := by { resetI, exact continuous f }
id └────────┘ ┴
src └────┘ └────┘└────────┘┴ ┴
typ └────┘ └────┘└────────┘┴┴┴
doc └────┘ └────┘└────────┘┴ ┴
txt └────┘ └────┘ ┴ ┴
par └────┘ └────┘ ┴ ┴
pid ┴ ┴ ┴
st └────────────────────────────┘└┘
253 | (n+1) E _ _ F _ _ f := by { resetI, exact differentiable 𝕜 f ∧ times_cont_diff_rec n (fderiv 𝕜 f) }
id ┴ └────────────┘ └─────────────────┘ ┴ └────┘ ┴ ┴
src ┴ └────┘ └────┘└────────────┘┴ ┴ ┴ ┴ ┴ ┴ └────┘┴ ┴ └┘
typ ┴ └────┘ └────┘└────────────┘┴ ┴ ┴ ┴└─────────────────┘┴┴┴ └────┘┴┴┴┴└┘
doc └────┘ └────┘└────────────┘┴ ┴ ┴ ┴ ┴ ┴ └────┘┴ ┴ └┘
txt └────┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
par └────┘ └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
pid ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴
st └───────────────────────────────────────────────────────────────────────┘└┘
254
255 @[simp] lemma times_cont_diff_rec_zero :
doc └──┘
256 times_cont_diff_rec 𝕜 0 f ↔ continuous f :=
id └─────────────────┘ ┴ ┴ ┴ └────────┘ ┴
src └─────────────────┘ ┴ └────────┘
typ └─────────────────┘ ┴ ┴ ┴ └────────┘ ┴
doc └─────────────────┘ └────────┘
257 by refl
src └────
typ └────
doc └────
txt └────
par └────
pid └
st └─────
258
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
259 @[simp] lemma times_cont_diff_rec_succ :
doc └──┘
260 times_cont_diff_rec 𝕜 n.succ f ↔
id └─────────────────┘ ┴ ┴└───┘ ┴ ┴
src └─────────────────┘ └───┘ ┴
typ └─────────────────┘ ┴ ┴└───┘ ┴ ┴
doc └─────────────────┘
261 differentiable 𝕜 f ∧ times_cont_diff_rec 𝕜 n (λx, fderiv 𝕜 f x) :=
id └────────────┘ ┴ ┴ ┴ └─────────────────┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴
src └────────────┘ ┴ └─────────────────┘ └────┘
typ └────────────┘ ┴ ┴ ┴ └─────────────────┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴
doc └────────────┘ └─────────────────┘ └────┘
262 by refl
src └────
typ └────
doc └────
txt └────
par └────
pid └
st └─────
263
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
264 lemma times_cont_diff_rec.of_succ (h : times_cont_diff_rec 𝕜 n.succ f) :
id └─────────────────┘ ┴ ┴└───┘ ┴
src └─────────────────┘ └───┘
typ └─────────────────┘ ┴ ┴└───┘ ┴
doc └─────────────────┘
265 times_cont_diff_rec 𝕜 n f :=
id └─────────────────┘ ┴ ┴ ┴
src └─────────────────┘
typ └─────────────────┘ ┴ ┴ ┴
doc └─────────────────┘
266 begin
st └─────
267 tactic.unfreeze_local_instances,
id └─────────────────────────────┘
src └─────────────────────────────┘
typ └─────────────────────────────┘
doc └─────────────────────────────┘
par └─────────────────────────────┘
st ───────────────────────────────────
268 induction n with n IH generalizing F,
id ┴
src └────────┘ └───────────────────────┘
typ └────────┘┴└───────────────────────┘
doc └────────┘ └───────────────────────┘
txt └────────┘ └───────────────────────┘
par └────────┘ └───────────────────────┘
pid ┴ ┴└───────┘└─────────────┘
st ─────────────────────────────────────┘└─
269 { exact h.1.continuous },
id ┴
src └────┘ └────────────┘
typ └────┘┴└────────────┘
doc └────┘ └────────────┘
txt └────┘ └────────────┘
par └────┘ └────────────┘
pid ┴ └──────────┘└┘
st ───┘└───────────────────┘└┘└
270 { rw times_cont_diff_rec_succ at h ⊢,
id └──────────────────────┘
src └─┘└──────────────────────┘└─────┘
typ └─┘└──────────────────────┘└─────┘
doc └─┘ └─────┘
txt └─┘ └─────┘
par └─┘ └─────┘
pid ┴ └─────┘
st ─────────────────────────────────────┘└─
271 exact ⟨h.1, IH h.2⟩ }
id └┘ ┴
src └────┘ └──┘ ┴ └──┘
typ └────┘ └──┘└┘┴┴└──┘
doc └────┘ └──┘ ┴ └──┘
txt └────┘ └──┘ ┴ └──┘
par └────┘ └──┘ ┴ └──┘
pid ┴ └──┘ ┴ └─┘┴
st ───────────────────────┘└─
272 end
st ──┘
273
274 lemma times_cont_diff_rec.continuous (h : times_cont_diff_rec 𝕜 n f) :
id └─────────────────┘ ┴ ┴ ┴
src └─────────────────┘
typ └─────────────────┘ ┴ ┴ ┴
doc └─────────────────┘
275 continuous (iterated_fderiv 𝕜 n f) :=
id └────────┘ └─────────────┘ ┴ ┴ ┴
src └────────┘ └─────────────┘
typ └────────┘ └─────────────┘ ┴ ┴ ┴
doc └────────┘ └─────────────┘
276 begin
st └─────
277 tactic.unfreeze_local_instances,
id └─────────────────────────────┘
src └─────────────────────────────┘
typ └─────────────────────────────┘
doc └─────────────────────────────┘
par └─────────────────────────────┘
st ───────────────────────────────────
278 induction n with n IH generalizing F f,
id ┴
src └────────┘ └─────────────────────────┘
typ └────────┘┴└─────────────────────────┘
doc └────────┘ └─────────────────────────┘
txt └────────┘ └─────────────────────────┘
par └────────┘ └─────────────────────────┘
pid ┴ ┴└───────┘└───────────────┘
st ───────────────────────────────────────┘└─
279 { exact h },
id ┴
src └────┘ ┴
typ └────┘┴┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───┘└──────┘└┘└
280 { rw iterated_fderiv_succ,
id └──────────────────┘
src └─┘└──────────────────┘
typ └─┘└──────────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ──────────────────────────┘└─
281 exact IH (times_cont_diff_rec_succ.1 h).2 }
id └┘ └──────────────────────┘ ┴
src └────┘ ┴ └──────────────────────┘└─┘ └──┘
typ └────┘└┘┴ └──────────────────────┘└─┘┴└──┘
doc └────┘ ┴ └─┘ └──┘
txt └────┘ ┴ └─┘ └──┘
par └────┘ ┴ └─┘ └──┘
pid ┴ ┴ └─┘ ┴└─┘
st ─────────────────────────────────────────────┘└─
282 end
st ──┘
283
284 lemma times_cont_diff_rec.differentiable (h : times_cont_diff_rec 𝕜 (n+1) f) :
id └─────────────────┘ ┴ ┴┴ ┴
src └─────────────────┘ ┴
typ └─────────────────┘ ┴ ┴┴ ┴
doc └─────────────────┘
285 differentiable 𝕜 (iterated_fderiv 𝕜 n f) :=
id └────────────┘ ┴ └─────────────┘ ┴ ┴ ┴
src └────────────┘ └─────────────┘
typ └────────────┘ ┴ └─────────────┘ ┴ ┴ ┴
doc └────────────┘ └─────────────┘
286 begin
st └─────
287 tactic.unfreeze_local_instances,
id └─────────────────────────────┘
src └─────────────────────────────┘
typ └─────────────────────────────┘
doc └─────────────────────────────┘
par └─────────────────────────────┘
st ───────────────────────────────────
288 induction n with n IH generalizing F f,
id ┴
src └────────┘ └─────────────────────────┘
typ └────────┘┴└─────────────────────────┘
doc └────────┘ └─────────────────────────┘
txt └────────┘ └─────────────────────────┘
par └────────┘ └─────────────────────────┘
pid ┴ ┴└───────┘└───────────────┘
st ───────────────────────────────────────┘└─
289 { exact h.1 },
id ┴
src └────┘ └─┘
typ └────┘┴└─┘
doc └────┘ └─┘
txt └────┘ └─┘
par └────┘ └─┘
pid ┴ └─┘
st ───┘└────────┘└┘└
290 { rw iterated_fderiv_succ,
id └──────────────────┘
src └─┘└──────────────────┘
typ └─┘└──────────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ──────────────────────────┘└─
291 apply IH h.2 }
id └┘ ┴
src └────┘ ┴ └─┘
typ └────┘└┘┴┴└─┘
doc └────┘ ┴ └─┘
txt └────┘ ┴ └─┘
par └────┘ ┴ └─┘
pid ┴ ┴ └─┘
st ────────────────┘└─
292 end
st ──┘
293
294 /--
295 Auxiliary definition defining `C^n` functions on a set by induction over `n`.
296 In applications, use `times_cont_diff_on` instead.
297 -/
298 def times_cont_diff_on_rec (𝕜 : Type w) [nondiscrete_normed_field 𝕜] :
id └──────────────────────┘ ┴
src └──────────────────────┘
typ └──────────────────────┘ ┴
doc └──────────────────────┘
299 Π (n : ℕ) {E : Type u} [gE : normed_group E] [@normed_space 𝕜 E _ gE]
id ┴ ┴ └──┘ └──────────┘ ┴ └──────────┘ ┴ ┴ └┘
src ┴ └──────────┘ └──────────┘
typ ┴ ┴ └──┘ └──────────┘ ┴ └──────────┘ ┴ ┴ └┘
doc └──────────┘ └──────────┘
300 {F : Type u} [gF : normed_group F] [@normed_space 𝕜 F _ gF] (f : E → F) (s : set E), Prop
id └──┘ └──────────┘ ┴ └──────────┘ ┴ ┴ └┘ ┴ ┴ ┴ └─┘ ┴
src └──────────┘ └──────────┘ └─┘
typ └──┘ └──────────┘ ┴ └──────────┘ ┴ ┴ └┘ ┴ ┴ ┴ └─┘ ┴
doc └──────────┘ └──────────┘
301 | 0 E _ _ F _ _ f s := by { resetI, exact continuous_on f s }
id └───────────┘ ┴ ┴
src └────┘ └────┘└───────────┘┴ ┴ ┴
typ └────┘ └────┘└───────────┘┴┴┴┴┴
doc └────┘ └────┘└───────────┘┴ ┴ ┴
txt └────┘ └────┘ ┴ ┴ ┴
par └────┘ └────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st └─────────────────────────────────┘└┘
302 | (n+1) E _ _ F _ _ f s := by { resetI,
id ┴
src ┴ └────┘
typ ┴ └────┘
doc └────┘
txt └────┘
par └────┘
st └──────────
303 exact differentiable_on 𝕜 f s ∧ times_cont_diff_on_rec n (fderiv_within 𝕜 f s) s}
id └───────────────┘ ┴ └────────────────────┘ ┴ └───────────┘ ┴ ┴ ┴
src └────┘└───────────────┘┴ ┴ ┴ ┴┴┴ ┴ ┴ └───────────┘┴ ┴ ┴ └┘
typ └────┘└───────────────┘┴ ┴ ┴ ┴┴┴└────────────────────┘┴┴┴ └───────────┘┴┴┴┴┴ └┘┴
doc └────┘└───────────────┘┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────────┘┴ ┴ ┴ └┘
txt └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
par └────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
pid ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
st ─────────────────────────────────────────────────────────────────────────────────────────────────┘└┘
304
305 @[simp] lemma times_cont_diff_on_rec_zero :
doc └──┘
306 times_cont_diff_on_rec 𝕜 0 f s ↔ continuous_on f s :=
id └────────────────────┘ ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴
src └────────────────────┘ ┴ └───────────┘
typ └────────────────────┘ ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴
doc └────────────────────┘ └───────────┘
307 by refl
src └────
typ └────
doc └────
txt └────
par └────
pid └
st └─────
308
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
309 @[simp] lemma times_cont_diff_on_rec_succ :
doc └──┘
310 times_cont_diff_on_rec 𝕜 n.succ f s ↔
id └────────────────────┘ ┴ ┴└───┘ ┴ ┴ ┴
src └────────────────────┘ └───┘ ┴
typ └────────────────────┘ ┴ ┴└───┘ ┴ ┴ ┴
doc └────────────────────┘
311 differentiable_on 𝕜 f s ∧ times_cont_diff_on_rec 𝕜 n (λx, fderiv_within 𝕜 f s x) s :=
id └───────────────┘ ┴ ┴ ┴ ┴ └────────────────────┘ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴
src └───────────────┘ ┴ └────────────────────┘ └───────────┘
typ └───────────────┘ ┴ ┴ ┴ ┴ └────────────────────┘ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴
doc └───────────────┘ └────────────────────┘ └───────────┘
312 by refl
src └────
typ └────
doc └────
txt └────
par └────
pid └
st └─────
313
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
314 lemma times_cont_diff_on_rec.of_succ (h : times_cont_diff_on_rec 𝕜 n.succ f s) :
id └────────────────────┘ ┴ ┴└───┘ ┴ ┴
src └────────────────────┘ └───┘
typ └────────────────────┘ ┴ ┴└───┘ ┴ ┴
doc └────────────────────┘
315 times_cont_diff_on_rec 𝕜 n f s :=
id └────────────────────┘ ┴ ┴ ┴ ┴
src └────────────────────┘
typ └────────────────────┘ ┴ ┴ ┴ ┴
doc └────────────────────┘
316 begin
st └─────
317 tactic.unfreeze_local_instances,
id └─────────────────────────────┘
src └─────────────────────────────┘
typ └─────────────────────────────┘
doc └─────────────────────────────┘
par └─────────────────────────────┘
st ───────────────────────────────────
318 induction n with n IH generalizing F,
id ┴
src └────────┘ └───────────────────────┘
typ └────────┘┴└───────────────────────┘
doc └────────┘ └───────────────────────┘
txt └────────┘ └───────────────────────┘
par └────────┘ └───────────────────────┘
pid ┴ ┴└───────┘└─────────────┘
st ─────────────────────────────────────┘└─
319 { exact h.1.continuous_on },
id ┴
src └────┘ └───────────────┘
typ └────┘┴└───────────────┘
doc └────┘ └───────────────┘
txt └────┘ └───────────────┘
par └────┘ └───────────────┘
pid ┴ └─────────────┘└┘
st ───┘└──────────────────────┘└┘└
320 { rw times_cont_diff_on_rec_succ at h ⊢,
id └─────────────────────────┘
src └─┘└─────────────────────────┘└─────┘
typ └─┘└─────────────────────────┘└─────┘
doc └─┘ └─────┘
txt └─┘ └─────┘
par └─┘ └─────┘
pid ┴ └─────┘
st ────────────────────────────────────────┘└─
321 exact ⟨h.1, IH h.2⟩ }
id └┘ ┴
src └────┘ └──┘ ┴ └──┘
typ └────┘ └──┘└┘┴┴└──┘
doc └────┘ └──┘ ┴ └──┘
txt └────┘ └──┘ ┴ └──┘
par └────┘ └──┘ ┴ └──┘
pid ┴ └──┘ ┴ └─┘┴
st ───────────────────────┘└─
322 end
st ──┘
323
324 lemma times_cont_diff_on_rec.continuous_on_iterated_fderiv_within
325 (h : times_cont_diff_on_rec 𝕜 n f s) :
id └────────────────────┘ ┴ ┴ ┴ ┴
src └────────────────────┘
typ └────────────────────┘ ┴ ┴ ┴ ┴
doc └────────────────────┘
326 continuous_on (iterated_fderiv_within 𝕜 n f s) s :=
id └───────────┘ └────────────────────┘ ┴ ┴ ┴ ┴ ┴
src └───────────┘ └────────────────────┘
typ └───────────┘ └────────────────────┘ ┴ ┴ ┴ ┴ ┴
doc └───────────┘ └────────────────────┘
327 begin
st └─────
328 tactic.unfreeze_local_instances,
id └─────────────────────────────┘
src └─────────────────────────────┘
typ └─────────────────────────────┘
doc └─────────────────────────────┘
par └─────────────────────────────┘
st ───────────────────────────────────
329 induction n with n IH generalizing F f,
id ┴
src └────────┘ └─────────────────────────┘
typ └────────┘┴└─────────────────────────┘
doc └────────┘ └─────────────────────────┘
txt └────────┘ └─────────────────────────┘
par └────────┘ └─────────────────────────┘
pid ┴ ┴└───────┘└───────────────┘
st ───────────────────────────────────────┘└─
330 { exact h },
id ┴
src └────┘ ┴
typ └────┘┴┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───┘└──────┘└┘└
331 { rw iterated_fderiv_within_succ,
id └─────────────────────────┘
src └─┘└─────────────────────────┘
typ └─┘└─────────────────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ─────────────────────────────────┘└─
332 exact IH (times_cont_diff_on_rec_succ.1 h).2 }
id └┘ └─────────────────────────┘ ┴
src └────┘ ┴ └─────────────────────────┘└─┘ └──┘
typ └────┘└┘┴ └─────────────────────────┘└─┘┴└──┘
doc └────┘ ┴ └─┘ └──┘
txt └────┘ ┴ └─┘ └──┘
par └────┘ ┴ └─┘ └──┘
pid ┴ ┴ └─┘ ┴└─┘
st ────────────────────────────────────────────────┘└─
333 end
st ──┘
334
335 lemma times_cont_diff_on_rec.differentiable_on (h : times_cont_diff_on_rec 𝕜 (n+1) f s) :
id └────────────────────┘ ┴ ┴┴ ┴ ┴
src └────────────────────┘ ┴
typ └────────────────────┘ ┴ ┴┴ ┴ ┴
doc └────────────────────┘
336 differentiable_on 𝕜 (iterated_fderiv_within 𝕜 n f s) s :=
id └───────────────┘ ┴ └────────────────────┘ ┴ ┴ ┴ ┴ ┴
src └───────────────┘ └────────────────────┘
typ └───────────────┘ ┴ └────────────────────┘ ┴ ┴ ┴ ┴ ┴
doc └───────────────┘ └────────────────────┘
337 begin
st └─────
338 tactic.unfreeze_local_instances,
id └─────────────────────────────┘
src └─────────────────────────────┘
typ └─────────────────────────────┘
doc └─────────────────────────────┘
par └─────────────────────────────┘
st ───────────────────────────────────
339 induction n with n IH generalizing F f,
id ┴
src └────────┘ └─────────────────────────┘
typ └────────┘┴└─────────────────────────┘
doc └────────┘ └─────────────────────────┘
txt └────────┘ └─────────────────────────┘
par └────────┘ └─────────────────────────┘
pid ┴ ┴└───────┘└───────────────┘
st ───────────────────────────────────────┘└─
340 { exact h.1 },
id ┴
src └────┘ └─┘
typ └────┘┴└─┘
doc └────┘ └─┘
txt └────┘ └─┘
par └────┘ └─┘
pid ┴ └─┘
st ───┘└────────┘└┘└
341 { rw iterated_fderiv_within_succ,
id └─────────────────────────┘
src └─┘└─────────────────────────┘
typ └─┘└─────────────────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ─────────────────────────────────┘└─
342 apply IH h.2 }
id └┘ ┴
src └────┘ ┴ └─┘
typ └────┘└┘┴┴└─┘
doc └────┘ ┴ └─┘
txt └────┘ ┴ └─┘
par └────┘ ┴ └─┘
pid ┴ ┴ └─┘
st ────────────────┘└─
343 end
st ──┘
344
345 lemma times_cont_diff_on_rec_univ :
346 times_cont_diff_on_rec 𝕜 n f univ ↔ times_cont_diff_rec 𝕜 n f :=
id └────────────────────┘ ┴ ┴ ┴ └──┘ ┴ └─────────────────┘ ┴ ┴ ┴
src └────────────────────┘ └──┘ ┴ └─────────────────┘
typ └────────────────────┘ ┴ ┴ ┴ └──┘ ┴ └─────────────────┘ ┴ ┴ ┴
doc └────────────────────┘ └─────────────────┘
347 begin
st └─────
348 tactic.unfreeze_local_instances,
id └─────────────────────────────┘
src └─────────────────────────────┘
typ └─────────────────────────────┘
doc └─────────────────────────────┘
par └─────────────────────────────┘
st ───────────────────────────────────
349 induction n with n IH generalizing F f,
id ┴
src └────────┘ └─────────────────────────┘
typ └────────┘┴└─────────────────────────┘
doc └────────┘ └─────────────────────────┘
txt └────────┘ └─────────────────────────┘
par └────────┘ └─────────────────────────┘
pid ┴ ┴└───────┘└───────────────┘
st ───────────────────────────────────────┘└─
350 { rw [times_cont_diff_on_rec_zero, times_cont_diff_rec_zero, continuous_iff_continuous_on_univ] },
id └─────────────────────────┘ └──────────────────────┘ └───────────────────────────────┘
src └──┘└─────────────────────────┘└┘└──────────────────────┘└┘└───────────────────────────────┘└┘
typ └──┘└─────────────────────────┘└┘└──────────────────────┘└┘└───────────────────────────────┘└┘
doc └──┘ └┘ └┘ └┘
txt └──┘ └┘ └┘ └┘
par └──┘ └┘ └┘ └┘
pid └┘ └┘ └┘ ┴┴
st ───┘└─────────────────────────────┘└────────────────────────┘└─────────────────────────────────┘┴┴└┘└
351 { rw [times_cont_diff_on_rec_succ, times_cont_diff_rec_succ, differentiable_on_univ, fderiv_within_univ, IH] }
id └─────────────────────────┘ └──────────────────────┘ └────────────────────┘ └────────────────┘
src └──┘└─────────────────────────┘└┘└──────────────────────┘└┘└────────────────────┘└┘└────────────────┘└┘ └┘
typ └──┘└─────────────────────────┘└┘└──────────────────────┘└┘└────────────────────┘└┘└────────────────┘└┘└┘└┘
doc └──┘ └┘ └┘ └┘ └┘ └┘
txt └──┘ └┘ └┘ └┘ └┘ └┘
par └──┘ └┘ └┘ └┘ └┘ └┘
pid └┘ └┘ └┘ └┘ └┘ ┴┴
st ──────────────────────────────────┘└────────────────────────┘└──────────────────────┘└──────────────────┘└──┘┴┴└─
352 end
st ──┘
353
354 /--
355 A function is `C^n` on a set, for `n : with_top ℕ`, if its derivatives of order at most `n`
356 are all well defined and continuous.
357 -/
358 def times_cont_diff_on (𝕜 : Type w) [nondiscrete_normed_field 𝕜] (n : with_top ℕ)
id └──────────────────────┘ ┴ └──────┘ ┴
src └──────────────────────┘ └──────┘ ┴
typ └──────────────────────┘ ┴ └──────┘ ┴
doc └──────────────────────┘
359 {E F : Type u} [normed_group E] [normed_space 𝕜 E]
id └──────────┘ ┴ └──────────┘ ┴ ┴
src └──────────┘ └──────────┘
typ └──────────┘ ┴ └──────────┘ ┴ ┴
doc └──────────┘ └──────────┘
360 [normed_group F] [normed_space 𝕜 F] (f : E → F) (s : set E) :=
id └──────────┘ ┴ └──────────┘ ┴ ┴ ┴ ┴ └─┘ ┴
src └──────────┘ └──────────┘ └─┘
typ └──────────┘ ┴ └──────────┘ ┴ ┴ ┴ ┴ └─┘ ┴
doc └──────────┘ └──────────┘
361 (∀m:ℕ, (m : with_top ℕ) ≤ n → continuous_on (iterated_fderiv_within 𝕜 m f s) s)
id ┴ ┴ └──────┘ ┴ ┴ ┴ └───────────┘ └────────────────────┘ ┴ ┴ ┴ ┴ ┴
src ┴ └──────┘ ┴ ┴ └───────────┘ └────────────────────┘
typ ┴ ┴ └──────┘ ┴ ┴ ┴ └───────────┘ └────────────────────┘ ┴ ┴ ┴ ┴ ┴
doc └───────────┘ └────────────────────┘
362 ∧ (∀m:ℕ, (m : with_top ℕ) < n → differentiable_on 𝕜 (iterated_fderiv_within 𝕜 m f s) s)
id ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ └───────────────┘ ┴ └────────────────────┘ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ └──────┘ ┴ ┴ └───────────────┘ └────────────────────┘
typ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ └───────────────┘ ┴ └────────────────────┘ ┴ ┴ ┴ ┴ ┴
doc └───────────────┘ └────────────────────┘
363
364 @[simp] lemma times_cont_diff_on_zero :
doc └──┘
365 times_cont_diff_on 𝕜 0 f s ↔ continuous_on f s :=
id └────────────────┘ ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴
src └────────────────┘ ┴ └───────────┘
typ └────────────────┘ ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴
doc └────────────────┘ └───────────┘
366 by simp [times_cont_diff_on]
id └────────────────┘
src └────┘└────────────────┘└─
typ └────┘└────────────────┘└─
doc └────┘└────────────────┘└─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └──────────────────────────
367
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
368 /--
369 The two definitions of `C^n` functions on domains, directly in terms of continuity of all
370 derivatives, or by induction, are equivalent.
371 -/
372 theorem times_cont_diff_on_iff_times_cont_diff_on_rec :
373 times_cont_diff_on 𝕜 n f s ↔ times_cont_diff_on_rec 𝕜 n f s :=
id └────────────────┘ ┴ ┴ ┴ ┴ ┴ └────────────────────┘ ┴ ┴ ┴ ┴
src └────────────────┘ ┴ └────────────────────┘
typ └────────────────┘ ┴ ┴ ┴ ┴ ┴ └────────────────────┘ ┴ ┴ ┴ ┴
doc └────────────────┘ └────────────────────┘
374 begin
st └─────
375 tactic.unfreeze_local_instances,
id └─────────────────────────────┘
src └─────────────────────────────┘
typ └─────────────────────────────┘
doc └─────────────────────────────┘
par └─────────────────────────────┘
st ───────────────────────────────────
376 induction n with n IH generalizing F f,
id ┴
src └────────┘ └─────────────────────────┘
typ └────────┘┴└─────────────────────────┘
doc └────────┘ └─────────────────────────┘
txt └────────┘ └─────────────────────────┘
par └────────┘ └─────────────────────────┘
pid ┴ ┴└───────┘└───────────────┘
st ───────────────────────────────────────┘└─
377 { rw [with_top.coe_zero, times_cont_diff_on_rec_zero, times_cont_diff_on_zero] },
id └───────────────┘ └─────────────────────────┘ └─────────────────────┘
src └──┘└───────────────┘└┘└─────────────────────────┘└┘└─────────────────────┘└┘
typ └──┘└───────────────┘└┘└─────────────────────────┘└┘└─────────────────────┘└┘
doc └──┘ └┘ └┘ └┘
txt └──┘ └┘ └┘ └┘
par └──┘ └┘ └┘ └┘
pid └┘ └┘ └┘ ┴┴
st ───┘└───────────────────┘└───────────────────────────┘└───────────────────────┘┴┴└┘└
378 { split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ────────┘└─
379 { assume H,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ─────┘└──────┘└─
380 rw times_cont_diff_on_rec_succ,
id └─────────────────────────┘
src └─┘└─────────────────────────┘
typ └─┘└─────────────────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ───────────────────────────────────┘└─
381 refine ⟨H.2 0 (by simp only [with_top.zero_lt_coe, with_top.coe_zero, nat.succ_pos n]), _⟩,
id ┴ └──────────────────┘ └───────────────┘ └──────────┘ ┴
src └─────┘ └───┘ ┴└─────────┘└──────────────────┘└┘└───────────────┘└┘└──────────┘┴ ┴└───┘
typ └─────┘ ┴└───┘ ┴└─────────┘└──────────────────┘└┘└───────────────┘└┘└──────────┘┴┴┴└───┘
doc └─────┘ └───┘ ┴└─────────┘ └┘ └┘ ┴ ┴└───┘
txt └─────┘ └───┘ ┴└─────────┘ └┘ └┘ ┴ ┴└───┘
par └─────┘ └───┘ ┴└─────────┘ └┘ └┘ ┴ ┴└───┘
pid ┴ └───┘ └──────────┘ └┘ └┘ ┴ └────┘
st ──────────────────────┘└──────────────────────────────────────────────────────────────────┘└───┘└─
382 rw ← IH,
src └───┘
typ └───┘└┘
doc └───┘
txt └───┘
par └───┘
pid └─┘
st ────────────┘└─
383 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────────┘└─
384 { assume m hm,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────────┘
st ───────┘└─────────┘└─
385 have : (m.succ : with_top nat) ≤ n.succ :=
id └────┘ └──────┘ └─┘ ┴ └────┘
src └─────┘ └────┘└─┘└──────┘┴└─┘└┘┴┴└────┘└───
typ └─────┘ └────┘└─┘└──────┘┴└─┘└┘┴┴└────┘└───
doc └─────┘ └─┘ ┴ └┘ ┴ └───
txt └─────┘ └─┘ ┴ └┘ ┴ └───
par └─────┘ └─┘ ┴ └┘ ┴ └───
pid └───┘└┘ └─┘ ┴ └┘ ┴ └───
st ───────────────────────────────────────────────────
386 with_top.coe_le_coe.2 (nat.succ_le_succ (with_top.coe_le_coe.1 hm)),
id └──────────────┘ └─────────────────┘ └┘
src ─────────┘ └─┘ └──────────────┘┴ └─────────────────┘└─┘ └┘
typ ─────────┘ └─┘ └──────────────┘┴ └─────────────────┘└─┘└┘└┘
doc ─────────┘ └─┘ ┴ └─┘ └┘
txt ─────────┘ └─┘ ┴ └─┘ └┘
par ─────────┘ └─┘ ┴ └─┘ └┘
pid ─────────┘ └─┘ ┴ └─┘ └┘
st ────────────────────────────────────────────────────────────────────────────┘└─
387 exact H.1 _ this },
id ┴ └──┘
src └────┘ └───┘ ┴
typ └────┘┴└───┘└──┘┴
doc └────┘ └───┘ ┴
txt └────┘ └───┘ ┴
par └────┘ └───┘ ┴
pid ┴ └───┘ ┴
st ────────────────────────┘└┘└
388 { assume m hm,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────────┘
st ──────────────────┘└─
389 have : (m.succ : with_top nat) < n.succ :=
id └────┘ └──────┘ └─┘ ┴ └────┘
src └─────┘ └────┘└─┘└──────┘┴└─┘└┘┴┴└────┘└───
typ └─────┘ └────┘└─┘└──────┘┴└─┘└┘┴┴└────┘└───
doc └─────┘ └─┘ ┴ └┘ ┴ └───
txt └─────┘ └─┘ ┴ └┘ ┴ └───
par └─────┘ └─┘ ┴ └┘ ┴ └───
pid └───┘└┘ └─┘ ┴ └┘ ┴ └───
st ───────────────────────────────────────────────────
390 with_top.coe_lt_coe.2 (nat.succ_le_succ (with_top.coe_lt_coe.1 hm)),
id └──────────────┘ └─────────────────┘ └┘
src ─────────┘ └─┘ └──────────────┘┴ └─────────────────┘└─┘ └┘
typ ─────────┘ └─┘ └──────────────┘┴ └─────────────────┘└─┘└┘└┘
doc ─────────┘ └─┘ ┴ └─┘ └┘
txt ─────────┘ └─┘ ┴ └─┘ └┘
par ─────────┘ └─┘ ┴ └─┘ └┘
pid ─────────┘ └─┘ ┴ └─┘ └┘
st ────────────────────────────────────────────────────────────────────────────┘└─
391 exact H.2 _ this } },
id ┴ └──┘
src └────┘ └───┘ ┴
typ └────┘┴└───┘└──┘┴
doc └────┘ └───┘ ┴
txt └────┘ └───┘ ┴
par └────┘ └───┘ ┴
pid ┴ └───┘ ┴
st ────────────────────────┘└──┘└
392 { assume H,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ─────────────┘└─
393 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────────┘└─
394 { assume m hm,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────────┘
st ───────┘└─────────┘└─
395 simp only [with_top.coe_le_coe] at hm,
id └─────────────────┘
src └─────────┘└─────────────────┘└─────┘
typ └─────────┘└─────────────────┘└─────┘
doc └─────────┘ └─────┘
txt └─────────┘ └─────┘
par └─────────┘ └─────┘
pid ┴└──┘└┘ ┴┴└───┘
st ────────────────────────────────────────────┘└─
396 cases nat.of_le_succ hm with h h,
id └────────────┘ └┘
src └────┘└────────────┘┴ └───────┘
typ └────┘└────────────┘┴└┘└───────┘
doc └────┘ ┴ └───────┘
txt └────┘ ┴ └───────┘
par └────┘ ┴ └───────┘
pid ┴ ┴ └───────┘
st ───────────────────────────────────────┘└─
397 { have := H.of_succ,
id └───────┘
src └──────┘└───────┘
typ └──────┘└───────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └───┘└─┘
st ─────────┘└───────────────┘└─
398 rw ← IH at this,
src └───┘ └──────┘
typ └───┘└┘└──────┘
doc └───┘ └──────┘
txt └───┘ └──────┘
par └───┘ └──────┘
pid └─┘ └──────┘
st ────────────────────────┘└─
399 exact this.1 _ (with_top.coe_le_coe.2 h) },
id └──┘ └─────────────────┘ ┴
src └────┘ └───┘ └─────────────────┘└─┘ └┘
typ └────┘└──┘└───┘ └─────────────────┘└─┘┴└┘
doc └────┘ └───┘ └─┘ └┘
txt └────┘ └───┘ └─┘ └┘
par └────┘ └───┘ └─┘ └┘
pid ┴ └───┘ └─┘ ┴┴
st ──────────────────────────────────────────────────┘└┘└
400 { rw h,
id ┴
src └─┘
typ └─┘┴
doc └─┘
txt └─┘
par └─┘
pid ┴
st ─────────────┘└─
401 simp at H,
src └───────┘
typ └───────┘
doc └───────┘
txt └───────┘
par └───────┘
pid ┴└──┘
st ──────────────────┘└─
402 exact H.2.continuous_on_iterated_fderiv_within } },
id ┴
src └────┘ └──────────────────────────────────────┘
typ └────┘┴└──────────────────────────────────────┘
doc └────┘ └──────────────────────────────────────┘
txt └────┘ └──────────────────────────────────────┘
par └────┘ └──────────────────────────────────────┘
pid ┴ └────────────────────────────────────┘└┘
st ────────────────────────────────────────────────────────┘└──┘└
403 { assume m hm,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────────┘
st ──────────────────┘└─
404 simp only [with_top.coe_lt_coe] at hm,
id └─────────────────┘
src └─────────┘└─────────────────┘└─────┘
typ └─────────┘└─────────────────┘└─────┘
doc └─────────┘ └─────┘
txt └─────────┘ └─────┘
par └─────────┘ └─────┘
pid ┴└──┘└┘ ┴┴└───┘
st ────────────────────────────────────────────┘└─
405 cases nat.of_le_succ hm with h h,
id └────────────┘ └┘
src └────┘└────────────┘┴ └───────┘
typ └────┘└────────────┘┴└┘└───────┘
doc └────┘ ┴ └───────┘
txt └────┘ ┴ └───────┘
par └────┘ ┴ └───────┘
pid ┴ ┴ └───────┘
st ───────────────────────────────────────┘└─
406 { have := H.of_succ,
id └───────┘
src └──────┘└───────┘
typ └──────┘└───────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └───┘└─┘
st ─────────┘└───────────────┘└─
407 rw ← IH at this,
src └───┘ └──────┘
typ └───┘└┘└──────┘
doc └───┘ └──────┘
txt └───┘ └──────┘
par └───┘ └──────┘
pid └─┘ └──────┘
st ────────────────────────┘└─
408 exact this.2 _ (with_top.coe_lt_coe.2 h) },
id └──┘ └─────────────────┘ ┴
src └────┘ └───┘ └─────────────────┘└─┘ └┘
typ └────┘└──┘└───┘ └─────────────────┘└─┘┴└┘
doc └────┘ └───┘ └─┘ └┘
txt └────┘ └───┘ └─┘ └┘
par └────┘ └───┘ └─┘ └┘
pid ┴ └───┘ └─┘ ┴┴
st ──────────────────────────────────────────────────┘└┘└
409 { rw nat.succ_inj h,
id └──────────┘ ┴
src └─┘└──────────┘┴
typ └─┘└──────────┘┴┴
doc └─┘ ┴
txt └─┘ ┴
par └─┘ ┴
pid ┴ ┴
st ──────────────────────────┘└─
410 exact H.differentiable_on } } } },
id └─────────────────┘
src └────┘└─────────────────┘┴
typ └────┘└─────────────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───────────────────────────────────┘└────────
411 end
st ──┘
412
413 /- Next lemma is marked as a simp lemma as `C^(n+1)` functions appear mostly in inductions. -/
414 @[simp] lemma times_cont_diff_on_succ :
doc └──┘
415 times_cont_diff_on 𝕜 n.succ f s ↔
id └────────────────┘ ┴ ┴└───┘ ┴ ┴ ┴
src └────────────────┘ └───┘ ┴
typ └────────────────┘ ┴ ┴└───┘ ┴ ┴ ┴
doc └────────────────┘
416 differentiable_on 𝕜 f s ∧ times_cont_diff_on 𝕜 n (λx, fderiv_within 𝕜 f s x) s :=
id └───────────────┘ ┴ ┴ ┴ ┴ └────────────────┘ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴
src └───────────────┘ ┴ └────────────────┘ └───────────┘
typ └───────────────┘ ┴ ┴ ┴ ┴ └────────────────┘ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴
doc └───────────────┘ └────────────────┘ └───────────┘
417 by simp [times_cont_diff_on_iff_times_cont_diff_on_rec]
id └───────────────────────────────────────────┘
src └────┘└───────────────────────────────────────────┘└─
typ └────┘└───────────────────────────────────────────┘└─
doc └────┘└───────────────────────────────────────────┘└─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └─────────────────────────────────────────────────────
418
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
419 lemma times_cont_diff_on.of_le {m n : with_top ℕ}
id └──────┘ ┴
src └──────┘ ┴
typ └──────┘ ┴
420 (h : times_cont_diff_on 𝕜 n f s) (le : m ≤ n) : times_cont_diff_on 𝕜 m f s :=
id └────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────────────────┘ ┴ ┴ ┴ ┴
src └────────────────┘ ┴ └────────────────┘
typ └────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────────────────┘ ┴ ┴ ┴ ┴
doc └────────────────┘ └────────────────┘
421 ⟨λp hp, h.1 p (le_trans hp le), λp hp, h.2 p (lt_of_lt_of_le hp le)⟩
id ┴ └┘ ┴┴ ┴ └──────┘ └┘ └┘ ┴ └┘ ┴┴ ┴ └────────────┘ └┘ └┘
src ┴ └──────┘ ┴ └────────────┘
typ ┴ └┘ ┴┴ ┴ └──────┘ └┘ └┘ ┴ └┘ ┴┴ ┴ └────────────┘ └┘ └┘
422
423 lemma times_cont_diff_on.of_succ (h : times_cont_diff_on 𝕜 n.succ f s) :
id └────────────────┘ ┴ ┴└───┘ ┴ ┴
src └────────────────┘ └───┘
typ └────────────────┘ ┴ ┴└───┘ ┴ ┴
doc └────────────────┘
424 times_cont_diff_on 𝕜 n f s :=
id └────────────────┘ ┴ ┴ ┴ ┴
src └────────────────┘
typ └────────────────┘ ┴ ┴ ┴ ┴
doc └────────────────┘
425 h.of_le (with_top.coe_le_coe.2 (nat.le_succ n))
id ┴└────┘ └─────────────────┘┴ └─────────┘ ┴
src └────┘ └─────────────────┘┴ └─────────┘
typ ┴└────┘ └─────────────────┘┴ └─────────┘ ┴
426
427 lemma times_cont_diff_on.continuous_on {n : with_top ℕ} (h : times_cont_diff_on 𝕜 n f s) :
id └──────┘ ┴ └────────────────┘ ┴ ┴ ┴ ┴
src └──────┘ ┴ └────────────────┘
typ └──────┘ ┴ └────────────────┘ ┴ ┴ ┴ ┴
doc └────────────────┘
428 continuous_on f s :=
id └───────────┘ ┴ ┴
src └───────────┘
typ └───────────┘ ┴ ┴
doc └───────────┘
429 h.1 0 (by simp)
id ┴┴
src ┴ └──┘
typ ┴┴ └──┘
doc └──┘
txt └──┘
par └──┘
st └───┘
430
431 lemma times_cont_diff_on.continuous_on_fderiv_within
432 {n : with_top ℕ} (h : times_cont_diff_on 𝕜 n f s) (hn : 1 ≤ n) :
id └──────┘ ┴ └────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └──────┘ ┴ └────────────────┘ ┴
typ └──────┘ ┴ └────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └────────────────┘
433 continuous_on (fderiv_within 𝕜 f s) s :=
id └───────────┘ └───────────┘ ┴ ┴ ┴ ┴
src └───────────┘ └───────────┘
typ └───────────┘ └───────────┘ ┴ ┴ ┴ ┴
doc └───────────┘ └───────────┘
434 h.1 1 hn
id ┴┴ └┘
src ┴
typ ┴┴ └┘
435
436 /-- If a function is at least C^1 on a set, it is differentiable there. -/
437 lemma times_cont_diff_on.differentiable_on
438 {n : with_top ℕ} (h : times_cont_diff_on 𝕜 n f s) (hn : 1 ≤ n) :
id └──────┘ ┴ └────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └──────┘ ┴ └────────────────┘ ┴
typ └──────┘ ┴ └────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └────────────────┘
439 differentiable_on 𝕜 f s :=
id └───────────────┘ ┴ ┴ ┴
src └───────────────┘
typ └───────────────┘ ┴ ┴ ┴
doc └───────────────┘
440 begin
st └─────
441 refine h.2 0 _,
id ┴
src └─────┘ └────┘
typ └─────┘┴└────┘
doc └─────┘ └────┘
txt └─────┘ └────┘
par └─────┘ └────┘
pid ┴ └────┘
st ───────────────┘└─
442 refine lt_of_lt_of_le _ hn,
id └────────────┘ └┘
src └─────┘└────────────┘└─┘
typ └─────┘└────────────┘└─┘└┘
doc └─────┘ └─┘
txt └─────┘ └─┘
par └─────┘ └─┘
pid ┴ └─┘
st ───────────────────────────┘└─
443 change ((0 : ℕ) : with_top ℕ) < (1 : ℕ),
id └──────┘ ┴
src └─────┘ └──┘ └──┘└──────┘┴ └┘┴┴ └──┘ ┴
typ └─────┘ └──┘ └──┘└──────┘┴ └┘┴┴ └──┘ ┴
doc └─────┘ └──┘ └──┘ ┴ └┘ ┴ └──┘ ┴
txt └─────┘ └──┘ └──┘ ┴ └┘ ┴ └──┘ ┴
par └─────┘ └──┘ └──┘ ┴ └┘ ┴ └──┘ ┴
pid ┴ └──┘ └──┘ ┴ └┘ ┴ └──┘ ┴
st ────────────────────────────────────────┘└─
444 rw with_top.coe_lt_coe,
id └─────────────────┘
src └─┘└─────────────────┘
typ └─┘└─────────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ───────────────────────┘└─
445 exact zero_lt_one
id └─────────┘
src └────┘└─────────┘┴
typ └────┘└─────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───────────────────┘
446 end
st └─┘
447
448 set_option class.instance_max_depth 50
doc └──────────────────────┘
449
450 /--
451 If a function is at least `C^1`, its bundled derivative (mapping `(x, v)` to `Df(x) v`) is
452 continuous.
453 -/
454 lemma times_cont_diff_on.continuous_on_fderiv_within_apply
455 {n : with_top ℕ} (h : times_cont_diff_on 𝕜 n f s) (hn : 1 ≤ n) :
id └──────┘ ┴ └────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └──────┘ ┴ └────────────────┘ ┴
typ └──────┘ ┴ └────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └────────────────┘
456 continuous_on (λp : E × E, (fderiv_within 𝕜 f s p.1 : E → F) p.2) (set.prod s univ) :=
id └───────────┘ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴┴ └──────┘ ┴ └──┘
src └───────────┘ ┴ └───────────┘ ┴ ┴ └──────┘ └──┘
typ └───────────┘ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴┴ └──────┘ ┴ └──┘
doc └───────────┘ └───────────┘ └──────┘
457 begin
st └─────
458 have A : continuous (λq : (E →L[𝕜] F) × E, q.1 q.2) := is_bounded_bilinear_map_apply.continuous,
id └────────┘ └─┘┴┴ ┴ ┴ ┴ └──────────────────────────────────────┘
src └───────┘└────────┘┴ └──┘ ┴└─┘ ┴┴ └┘┴┴ └┘ └─┘ └─────┘└──────────────────────────────────────┘
typ └───────┘└────────┘┴ └──┘ ┴└─┘┴┴┴┴└┘┴┴┴└┘ └─┘ └─────┘└──────────────────────────────────────┘
doc └───────┘└────────┘┴ └──┘ ┴└─┘ ┴┴ └┘ ┴ └┘ └─┘ └─────┘
txt └───────┘ ┴ └──┘ ┴ ┴ └┘ ┴ └┘ └─┘ └─────┘
par └───────┘ ┴ └──┘ ┴ ┴ └┘ ┴ └┘ └─┘ └─────┘
pid └────┘└─┘ ┴ └──┘ ┴ ┴ └┘ ┴ └┘ └─┘ └─┘└──┘
st ────────────────────────────────────────────────────────────────────────────────────────────────┘└─
459 have B : continuous_on (λp : E × E, (fderiv_within 𝕜 f s p.1, p.2)) (set.prod s univ),
id └───────────┘ ┴ ┴ ┴└───────────┘ ┴ ┴ └──────┘ ┴ └──┘
src └───────┘└───────────┘┴ └──┘ ┴ ┴ └┘┴└───────────┘┴ ┴ ┴ ┴ └──┘ └───┘ └──────┘┴ ┴└──┘┴
typ └───────┘└───────────┘┴ └──┘ ┴┴┴┴└┘┴└───────────┘┴┴┴┴┴ ┴ └──┘ └───┘ └──────┘┴┴┴└──┘┴
doc └───────┘└───────────┘┴ └──┘ ┴ ┴ └┘ └───────────┘┴ ┴ ┴ ┴ └──┘ └───┘ └──────┘┴ ┴ ┴
txt └───────┘ ┴ └──┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └──┘ └───┘ ┴ ┴ ┴
par └───────┘ ┴ └──┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └──┘ └───┘ ┴ ┴ ┴
pid └────┘└─┘ ┴ └──┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └──┘ └───┘ ┴ ┴ ┴
st ──────────────────────────────────────────────────────────────────────────────────────┘└─
460 { apply continuous_on.prod _ continuous_snd.continuous_on,
id └────────────────┘ └──────────────────────────┘
src └────┘└────────────────┘└─┘└──────────────────────────┘
typ └────┘└────────────────┘└─┘└──────────────────────────┘
doc └────┘ └─┘
txt └────┘ └─┘
par └────┘ └─┘
pid ┴ └─┘
st ───┘└─────────────────────────────────────────────────────┘└─
461 exact continuous_on.comp (h.continuous_on_fderiv_within hn) continuous_fst.continuous_on
id └────────────────┘ └───────────────────────────┘ └┘ └──────────────────────────┘
src └────┘└────────────────┘┴ └───────────────────────────┘┴ └┘└──────────────────────────┘└
typ └────┘└────────────────┘┴ └───────────────────────────┘┴└┘└┘└──────────────────────────┘└
doc └────┘ ┴ ┴ └┘ └
txt └────┘ ┴ ┴ └┘ └
par └────┘ ┴ ┴ └┘ └
pid ┴ ┴ ┴ └┘ └
st ─────────────────────────────────────────────────────────────────────────────────────────────
462 (prod_subset_preimage_fst _ _) },
id └──────────────────────┘
src ─────┘ └──────────────────────┘└────┘
typ ─────┘ └──────────────────────┘└────┘
doc ─────┘ └────┘
txt ─────┘ └────┘
par ─────┘ └────┘
pid ─────┘ └───┘┴
st ────────────────────────────────────┘└┘└
463 exact A.comp_continuous_on B
id └──────────────────┘ ┴
src └────┘└──────────────────┘┴ ┴
typ └────┘└──────────────────┘┴┴┴
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ──────────────────────────────┘
464 end
st └─┘
465
466 lemma times_cont_diff_on_top :
467 times_cont_diff_on 𝕜 ⊤ f s ↔ (∀n:ℕ, times_cont_diff_on 𝕜 n f s) :=
id └────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────────────────┘ ┴ ┴ ┴ ┴
src └────────────────┘ ┴ ┴ ┴ └────────────────┘
typ └────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────────────────┘ ┴ ┴ ┴ ┴
doc └────────────────┘ └────────────────┘
468 begin
st └─────
469 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────┘└─
470 { assume h n,
src └────────┘
typ └────────┘
doc └────────┘
txt └────────┘
par └────────┘
pid └────────┘
st ───┘└────────┘└─
471 exact h.of_le lattice.le_top },
id └─────┘ └────────────┘
src └────┘└─────┘┴└────────────┘┴
typ └────┘└─────┘┴└────────────┘┴
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ────────────────────────────────┘└┘└
472 { assume h,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ───────────┘└─
473 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ────────┘└─
474 { exact λm hm, (h m).1 m (le_refl _) },
id ┴ └─────┘
src └────┘ └────┘ ┴ └──┘ ┴ └─────┘└──┘
typ └────┘ └────┘ ┴┴ └──┘ ┴ └─────┘└──┘
doc └────┘ └────┘ ┴ └──┘ ┴ └──┘
txt └────┘ └────┘ ┴ └──┘ ┴ └──┘
par └────┘ └────┘ ┴ └──┘ ┴ └──┘
pid ┴ └────┘ ┴ └──┘ ┴ └─┘┴
st ─────┘└─────────────────────────────────┘└┘└
475 { exact λ m hm, (h m.succ).2 m (with_top.coe_lt_coe.2 (lt_add_one m)) } }
id ┴ └───┘ └─────────────────┘ └────────┘
src └────┘ └─────┘ ┴ └───┘└──┘ ┴ └─────────────────┘└─┘ └────────┘┴ └─┘
typ └────┘ └─────┘ ┴┴ └───┘└──┘ ┴ └─────────────────┘└─┘ └────────┘┴ └─┘
doc └────┘ └─────┘ ┴ └──┘ ┴ └─┘ ┴ └─┘
txt └────┘ └─────┘ ┴ └──┘ ┴ └─┘ ┴ └─┘
par └────┘ └─────┘ ┴ └──┘ ┴ └─┘ ┴ └─┘
pid ┴ └─────┘ ┴ └──┘ ┴ └─┘ ┴ └┘┴
st ─────────────────────────────────────────────────────────────────────────┘└───
476 end
st ──┘
477
478 lemma times_cont_diff_on_fderiv_within_nat {m n : ℕ}
id ┴
src ┴
typ ┴
479 (hf : times_cont_diff_on 𝕜 n f s) (h : m + 1 ≤ n) :
id └────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └────────────────┘ ┴ ┴
typ └────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └────────────────┘
480 times_cont_diff_on 𝕜 m (λx, fderiv_within 𝕜 f s x) s :=
id └────────────────┘ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴
src └────────────────┘ └───────────┘
typ └────────────────┘ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴
doc └────────────────┘ └───────────┘
481 begin
st └─────
482 have : times_cont_diff_on 𝕜 m.succ f s :=
id └────────────────┘ ┴ └────┘ ┴ ┴
src └─────┘└────────────────┘┴ ┴└────┘┴ ┴ └───
typ └─────┘└────────────────┘┴┴┴└────┘┴┴┴┴└───
doc └─────┘└────────────────┘┴ ┴ ┴ ┴ └───
txt └─────┘ ┴ ┴ ┴ ┴ └───
par └─────┘ ┴ ┴ ┴ ┴ └───
pid └───┘└┘ ┴ ┴ ┴ ┴ └───
st ────────────────────────────────────────────
483 hf.of_le (with_top.coe_le_coe.2 h),
id └──────┘ └─────────────────┘ ┴
src ───┘└──────┘┴ └─────────────────┘└─┘ ┴
typ ───┘└──────┘┴ └─────────────────┘└─┘┴┴
doc ───┘ ┴ └─┘ ┴
txt ───┘ ┴ └─┘ ┴
par ───┘ ┴ └─┘ ┴
pid ───┘ ┴ └─┘ ┴
st ─────────────────────────────────────┘└─
484 exact (times_cont_diff_on_succ.1 this).2
id └─────────────────────┘ └──┘
src └────┘ └─────────────────────┘└─┘ └──┘
typ └────┘ └─────────────────────┘└─┘└──┘└──┘
doc └────┘ └─┘ └──┘
txt └────┘ └─┘ └──┘
par └────┘ └─┘ └──┘
pid ┴ └─┘ ┴└─┘
st ──────────────────────────────────────────┘
485 end
st └─┘
486
487 lemma times_cont_diff_on_fderiv_within {m n : with_top ℕ}
id └──────┘ ┴
src └──────┘ ┴
typ └──────┘ ┴
488 (hf : times_cont_diff_on 𝕜 n f s) (h : m + 1 ≤ n) :
id └────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └────────────────┘ ┴ ┴
typ └────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └────────────────┘
489 times_cont_diff_on 𝕜 m (λx, fderiv_within 𝕜 f s x) s :=
id └────────────────┘ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴
src └────────────────┘ └───────────┘
typ └────────────────┘ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴
doc └────────────────┘ └───────────┘
490 begin
st └─────
491 cases m,
id ┴
src └────┘
typ └────┘┴
doc └────┘
txt └────┘
par └────┘
pid ┴
st ────────┘└─
492 { change ⊤ + 1 ≤ n at h,
id ┴ ┴ ┴ ┴
src └─────┘┴┴┴└─┘┴┴ └───┘
typ └─────┘┴┴┴└─┘┴┴┴└───┘
doc └─────┘ ┴ └─┘ ┴ └───┘
txt └─────┘ ┴ └─┘ ┴ └───┘
par └─────┘ ┴ └─┘ ┴ └───┘
pid ┴ ┴ └─┘ ┴ ┴└──┘
st ───┘└───────────────────┘└─
493 have : n = ⊤, by simpa using h,
id ┴ ┴ ┴
src └─────┘ ┴┴┴ └──────────┘
typ └─────┘┴┴┴┴ └──────────┘┴
doc └─────┘ ┴ ┴ └──────────┘
txt └─────┘ ┴ ┴ └──────────┘
par └─────┘ ┴ ┴ └──────────┘
pid └───┘└┘ ┴ ┴ ┴└────┘
st ───────────────┘ └─
494 rw this at hf,
id └──┘
src └─┘ └────┘
typ └─┘└──┘└────┘
doc └─┘ └────┘
txt └─┘ └────┘
par └─┘ └────┘
pid ┴ └────┘
st ────────────────┘└─
495 change times_cont_diff_on 𝕜 ⊤ (λ (x : E), fderiv_within 𝕜 f s x) s,
id └────────────────┘ ┴ └───────────┘ ┴ ┴ ┴
src └─────┘└────────────────┘┴ ┴ ┴ └────┘ └─┘└───────────┘┴ ┴ ┴ ┴ └┘
typ └─────┘└────────────────┘┴ ┴ ┴ └────┘┴└─┘└───────────┘┴┴┴┴┴ ┴ └┘┴
doc └─────┘└────────────────┘┴ ┴ ┴ └────┘ └─┘└───────────┘┴ ┴ ┴ ┴ └┘
txt └─────┘ ┴ ┴ ┴ └────┘ └─┘ ┴ ┴ ┴ ┴ └┘
par └─────┘ ┴ ┴ ┴ └────┘ └─┘ ┴ ┴ ┴ ┴ └┘
pid ┴ ┴ ┴ ┴ └────┘ └─┘ ┴ ┴ ┴ ┴ └┘
st ─────────────────────────────────────────────────────────────────────┘└─
496 rw times_cont_diff_on_top at ⊢ hf,
id └────────────────────┘
src └─┘└────────────────────┘└──────┘
typ └─┘└────────────────────┘└──────┘
doc └─┘ └──────┘
txt └─┘ └──────┘
par └─┘ └──────┘
pid ┴ └──────┘
st ────────────────────────────────────┘└─
497 exact λm, times_cont_diff_on_fderiv_within_nat (hf (m + 1)) (le_refl _) },
id └──────────────────────────────────┘ └┘ └─────┘
src └────┘ └─┘└──────────────────────────────────┘┴ ┴ ┴ └───┘ └─────┘└──┘
typ └────┘ └─┘└──────────────────────────────────┘┴ └┘┴ ┴ └───┘ └─────┘└──┘
doc └────┘ └─┘ ┴ ┴ ┴ └───┘ └──┘
txt └────┘ └─┘ ┴ ┴ ┴ └───┘ └──┘
par └────┘ └─┘ ┴ ┴ ┴ └───┘ └──┘
pid ┴ └─┘ ┴ ┴ ┴ └───┘ └─┘┴
st ───────────────────────────────────────────────────────────────────────────┘└┘└
498 { have : times_cont_diff_on 𝕜 (m + 1) f s := hf.of_le h,
id └────────────────┘ ┴ ┴ ┴ ┴ └──────┘ ┴
src └─────┘└────────────────┘┴ ┴ ┴ └──┘ ┴ └──┘└──────┘┴
typ └─────┘└────────────────┘┴┴┴ ┴┴ └──┘┴┴┴└──┘└──────┘┴┴
doc └─────┘└────────────────┘┴ ┴ ┴ └──┘ ┴ └──┘ ┴
txt └─────┘ ┴ ┴ ┴ └──┘ ┴ └──┘ ┴
par └─────┘ ┴ ┴ ┴ └──┘ ┴ └──┘ ┴
pid └───┘└┘ ┴ ┴ ┴ └──┘ ┴ └──┘ ┴
st ────────────────────────────────────────────────────────┘└─
499 exact times_cont_diff_on_fderiv_within_nat this (le_refl _) }
id └──────────────────────────────────┘ └──┘ └─────┘
src └────┘└──────────────────────────────────┘┴ ┴ └─────┘└──┘
typ └────┘└──────────────────────────────────┘┴└──┘┴ └─────┘└──┘
doc └────┘ ┴ ┴ └──┘
txt └────┘ ┴ ┴ └──┘
par └────┘ ┴ ┴ └──┘
pid ┴ ┴ ┴ └─┘┴
st ───────────────────────────────────────────────────────────────┘└─
500 end
st ──┘
501
502 lemma times_cont_diff_on.congr_mono {n : with_top ℕ} (H : times_cont_diff_on 𝕜 n f s)
id └──────┘ ┴ └────────────────┘ ┴ ┴ ┴ ┴
src └──────┘ ┴ └────────────────┘
typ └──────┘ ┴ └────────────────┘ ┴ ┴ ┴ ┴
doc └────────────────┘
503 (hs : unique_diff_on 𝕜 s₁) (h : ∀x ∈ s₁, f₁ x = f x) (h₁ : s₁ ⊆ s) :
id └────────────┘ ┴ └┘ ┴ └┘ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴
src └────────────┘ ┴ ┴
typ └────────────┘ ┴ └┘ ┴ └┘ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴
doc └────────────┘
504 times_cont_diff_on 𝕜 n f₁ s₁ :=
id └────────────────┘ ┴ ┴ └┘ └┘
src └────────────────┘
typ └────────────────┘ ┴ ┴ └┘ └┘
doc └────────────────┘
505 begin
st └─────
506 tactic.unfreeze_local_instances,
id └─────────────────────────────┘
src └─────────────────────────────┘
typ └─────────────────────────────┘
doc └─────────────────────────────┘
par └─────────────────────────────┘
st ───────────────────────────────────
507 induction n using with_top.nat_induction with n IH Itop generalizing F,
id ┴
src └────────┘ └─────────────────────────────────────────────────────────┘
typ └────────┘┴└─────────────────────────────────────────────────────────┘
doc └────────┘ └─────────────────────────────────────────────────────────┘
txt └────────┘ └─────────────────────────────────────────────────────────┘
par └────────┘ └─────────────────────────────────────────────────────────┘
pid ┴ └───────────────────────────┘└─────────────┘└─────────────┘
st ───────────────────────────────────────────────────────────────────────┘└─
508 { rw times_cont_diff_on_zero at H ⊢,
id └─────────────────────┘
src └─┘└─────────────────────┘└─────┘
typ └─┘└─────────────────────┘└─────┘
doc └─┘ └─────┘
txt └─┘ └─────┘
par └─┘ └─────┘
pid ┴ └─────┘
st ───┘└───────────────────────────────┘└─
509 exact continuous_on.congr_mono H h h₁ },
id └──────────────────────┘ ┴ ┴ └┘
src └────┘└──────────────────────┘┴ ┴ ┴ ┴
typ └────┘└──────────────────────┘┴┴┴┴┴└┘┴
doc └────┘ ┴ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴
st ─────────────────────────────────────────┘└┘└
510 { rw times_cont_diff_on_succ at H ⊢,
id └─────────────────────┘
src └─┘└─────────────────────┘└─────┘
typ └─┘└─────────────────────┘└─────┘
doc └─┘ └─────┘
txt └─┘ └─────┘
par └─┘ └─────┘
pid ┴ └─────┘
st ───┘└───────────────────────────────┘└─
511 refine ⟨differentiable_on.congr_mono H.1 h h₁, IH H.2 (λx hx, _)⟩,
id └──────────────────────────┘ ┴ └┘ └┘ ┴
src └─────┘ └──────────────────────────┘┴ └─┘ ┴ └┘ ┴ └─┘ └───────┘
typ └─────┘ └──────────────────────────┘┴ └─┘┴┴└┘└┘└┘┴┴└─┘ └───────┘
doc └─────┘ ┴ └─┘ ┴ └┘ ┴ └─┘ └───────┘
txt └─────┘ ┴ └─┘ ┴ └┘ ┴ └─┘ └───────┘
par └─────┘ ┴ └─┘ ┴ └┘ ┴ └─┘ └───────┘
pid ┴ ┴ └─┘ ┴ └┘ ┴ └─┘ └───────┘
st ────────────────────────────────────────────────────────────────────┘└─
512 apply differentiable_within_at.fderiv_within_congr_mono
id └───────────────────────────────────────────────┘
src └────┘└───────────────────────────────────────────────┘└
typ └────┘└───────────────────────────────────────────────┘└
doc └────┘ └
txt └────┘ └
par └────┘ └
pid ┴ └
st ────────────────────────────────────────────────────────────
513 (H.1 x (h₁ hx)) h (h x hx) (hs x hx) h₁ },
id ┴ ┴ └┘ ┴ └┘ └┘
src ─────┘ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴
typ ─────┘ ┴└─┘ ┴ ┴ └─┘ ┴ ┴┴ ┴ └┘ └┘┴┴┴└┘└┘└┘┴
doc ─────┘ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴
txt ─────┘ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴
par ─────┘ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴
pid ─────┘ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴ └┘ ┴ ┴ └┘ ┴
st ─────────────────────────────────────────────┘└┘└
514 { rw times_cont_diff_on_top at H ⊢,
id └────────────────────┘
src └─┘└────────────────────┘└─────┘
typ └─┘└────────────────────┘└─────┘
doc └─┘ └─────┘
txt └─┘ └─────┘
par └─┘ └─────┘
pid ┴ └─────┘
st ───────────────────────────────────┘└─
515 assume n, exact Itop n (H n) h }
id └──┘ ┴ ┴ ┴
src └──────┘ └────┘ ┴ ┴ ┴ └┘ ┴
typ └──────┘ └────┘└──┘┴ ┴ ┴┴┴└┘┴┴
doc └──────┘ └────┘ ┴ ┴ ┴ └┘ ┴
txt └──────┘ └────┘ ┴ ┴ ┴ └┘ ┴
par └──────┘ └────┘ ┴ ┴ ┴ └┘ ┴
pid └──────┘ ┴ ┴ ┴ ┴ └┘ ┴
st ───────────┘└─────────────────────┘└─
516 end
st ──┘
517
518 lemma times_cont_diff_on.congr {n : with_top ℕ} {s : set E} (H : times_cont_diff_on 𝕜 n f s)
id └──────┘ ┴ └─┘ ┴ └────────────────┘ ┴ ┴ ┴ ┴
src └──────┘ ┴ └─┘ └────────────────┘
typ └──────┘ ┴ └─┘ ┴ └────────────────┘ ┴ ┴ ┴ ┴
doc └────────────────┘
519 (hs : unique_diff_on 𝕜 s) (h : ∀x ∈ s, f₁ x = f x) :
id └────────────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
src └────────────┘ ┴
typ └────────────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
doc └────────────┘
520 times_cont_diff_on 𝕜 n f₁ s :=
id └────────────────┘ ┴ ┴ └┘ ┴
src └────────────────┘
typ └────────────────┘ ┴ ┴ └┘ ┴
doc └────────────────┘
521 times_cont_diff_on.congr_mono H hs h (subset.refl _)
id └───────────────────────────┘ ┴ └┘ ┴ └─────────┘
src └───────────────────────────┘ └─────────┘
typ └───────────────────────────┘ ┴ └┘ ┴ └─────────┘
522
523 lemma times_cont_diff_on.congr_mono' {n m : with_top ℕ} {s : set E} (H : times_cont_diff_on 𝕜 n f s)
id └──────┘ ┴ └─┘ ┴ └────────────────┘ ┴ ┴ ┴ ┴
src └──────┘ ┴ └─┘ └────────────────┘
typ └──────┘ ┴ └─┘ ┴ └────────────────┘ ┴ ┴ ┴ ┴
doc └────────────────┘
524 (hs : unique_diff_on 𝕜 s₁) (h : ∀x ∈ s₁, f₁ x = f x) (h₁ : s₁ ⊆ s) (le : m ≤ n) :
id └────────────┘ ┴ └┘ ┴ └┘ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴
src └────────────┘ ┴ ┴ ┴
typ └────────────┘ ┴ └┘ ┴ └┘ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴
doc └────────────┘
525 times_cont_diff_on 𝕜 m f₁ s₁ :=
id └────────────────┘ ┴ ┴ └┘ └┘
src └────────────────┘
typ └────────────────┘ ┴ ┴ └┘ └┘
doc └────────────────┘
526 times_cont_diff_on.of_le (H.congr_mono hs h h₁) le
id └──────────────────────┘ ┴└─────────┘ └┘ ┴ └┘ └┘
src └──────────────────────┘ └─────────┘
typ └──────────────────────┘ ┴└─────────┘ └┘ ┴ └┘ └┘
527
528 lemma times_cont_diff_on.mono {n : with_top ℕ} {s t : set E} (h : times_cont_diff_on 𝕜 n f t)
id └──────┘ ┴ └─┘ ┴ └────────────────┘ ┴ ┴ ┴ ┴
src └──────┘ ┴ └─┘ └────────────────┘
typ └──────┘ ┴ └─┘ ┴ └────────────────┘ ┴ ┴ ┴ ┴
doc └────────────────┘
529 (hst : s ⊆ t) (hs : unique_diff_on 𝕜 s) : times_cont_diff_on 𝕜 n f s :=
id ┴ ┴ ┴ └────────────┘ ┴ ┴ └────────────────┘ ┴ ┴ ┴ ┴
src ┴ └────────────┘ └────────────────┘
typ ┴ ┴ ┴ └────────────┘ ┴ ┴ └────────────────┘ ┴ ┴ ┴ ┴
doc └────────────┘ └────────────────┘
530 times_cont_diff_on.congr_mono h hs (λx hx, rfl) hst
id └───────────────────────────┘ ┴ └┘ ┴ └┘ └─┘ └─┘
src └───────────────────────────┘ └─┘
typ └───────────────────────────┘ ┴ └┘ ┴ └┘ └─┘ └─┘
531
532 /--
533 Being `C^n` is a local property.
534 -/
535 lemma times_cont_diff_on_of_locally_times_cont_diff_on {n : with_top ℕ} {s : set E}
id └──────┘ ┴ └─┘ ┴
src └──────┘ ┴ └─┘
typ └──────┘ ┴ └─┘ ┴
536 (hs : unique_diff_on 𝕜 s) (h : ∀x∈s, ∃u, is_open u ∧ x ∈ u ∧ times_cont_diff_on 𝕜 n f (s ∩ u)) :
id └────────────┘ ┴ ┴ ┴ ┴ ┴┴┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └────────────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ └────────────────┘ ┴
typ └────────────┘ ┴ ┴ ┴ ┴ ┴┴┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └────────────┘ └─────┘ └────────────────┘
537 times_cont_diff_on 𝕜 n f s :=
id └────────────────┘ ┴ ┴ ┴ ┴
src └────────────────┘
typ └────────────────┘ ┴ ┴ ┴ ┴
doc └────────────────┘
538 begin
st └─────
539 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────┘└─
540 { assume m hm,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────────┘
st ───┘└─────────┘└─
541 apply continuous_on_of_locally_continuous_on (λx hx, _),
id └────────────────────────────────────┘
src └────┘└────────────────────────────────────┘┴ └──────┘
typ └────┘└────────────────────────────────────┘┴ └──────┘
doc └────┘ ┴ └──────┘
txt └────┘ ┴ └──────┘
par └────┘ ┴ └──────┘
pid ┴ ┴ └──────┘
st ──────────────────────────────────────────────────────────┘└─
542 rcases h x hx with ⟨u, u_open, xu, hu⟩,
id ┴ ┴ └┘
src └─────┘ ┴ ┴ └───────────────────────┘
typ └─────┘┴┴┴┴└┘└───────────────────────┘
doc └─────┘ ┴ ┴ └───────────────────────┘
txt └─────┘ ┴ ┴ └───────────────────────┘
par └─────┘ ┴ ┴ └───────────────────────┘
pid ┴ ┴ ┴ └───────────────────────┘
st ─────────────────────────────────────────┘└─
543 refine ⟨u, u_open, xu,_⟩,
id ┴ └────┘ └┘
src └─────┘ └┘ └┘ └─┘
typ └─────┘ ┴└┘└────┘└┘└┘└─┘
doc └─────┘ └┘ └┘ └─┘
txt └─────┘ └┘ └┘ └─┘
par └─────┘ └┘ └┘ └─┘
pid ┴ └┘ └┘ └─┘
st ───────────────────────────┘└─
544 apply continuous_on.congr_mono (hu.1 m hm) (λy hy, _) (subset.refl _),
id └──────────────────────┘ └┘ ┴ └┘ └─────────┘
src └────┘└──────────────────────┘┴ └─┘ ┴ └┘ └───────┘ └─────────┘└─┘
typ └────┘└──────────────────────┘┴ └┘└─┘┴┴└┘└┘ └───────┘ └─────────┘└─┘
doc └────┘ ┴ └─┘ ┴ └┘ └───────┘ └─┘
txt └────┘ ┴ └─┘ ┴ └┘ └───────┘ └─┘
par └────┘ ┴ └─┘ ┴ └┘ └───────┘ └─┘
pid ┴ ┴ └─┘ ┴ └┘ └───────┘ └─┘
st ────────────────────────────────────────────────────────────────────────┘└─
545 symmetry,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
st ───────────┘└─
546 exact iterated_fderiv_within_inter_open hy.2 u_open hy.1 (hs.inter u_open) },
id └───────────────────────────────┘ └┘ └──────┘ └────┘
src └────┘└───────────────────────────────┘┴ └─┘ ┴ └─┘ └──────┘┴ └┘
typ └────┘└───────────────────────────────┘┴ └─┘ ┴└┘└─┘ └──────┘┴└────┘└┘
doc └────┘└───────────────────────────────┘┴ └─┘ ┴ └─┘ ┴ └┘
txt └────┘ ┴ └─┘ ┴ └─┘ ┴ └┘
par └────┘ ┴ └─┘ ┴ └─┘ ┴ └┘
pid ┴ ┴ └─┘ ┴ └─┘ ┴ ┴┴
st ──────────────────────────────────────────────────────────────────────────────┘└┘└
547 { assume m hm,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────────┘
st ──────────────┘└─
548 apply differentiable_on_of_locally_differentiable_on (λx hx, _),
id └────────────────────────────────────────────┘
src └────┘└────────────────────────────────────────────┘┴ └──────┘
typ └────┘└────────────────────────────────────────────┘┴ └──────┘
doc └────┘ ┴ └──────┘
txt └────┘ ┴ └──────┘
par └────┘ ┴ └──────┘
pid ┴ ┴ └──────┘
st ──────────────────────────────────────────────────────────────────┘└─
549 rcases h x hx with ⟨u, u_open, xu, hu⟩,
id ┴ ┴ └┘
src └─────┘ ┴ ┴ └───────────────────────┘
typ └─────┘┴┴┴┴└┘└───────────────────────┘
doc └─────┘ ┴ ┴ └───────────────────────┘
txt └─────┘ ┴ ┴ └───────────────────────┘
par └─────┘ ┴ ┴ └───────────────────────┘
pid ┴ ┴ ┴ └───────────────────────┘
st ─────────────────────────────────────────┘└─
550 refine ⟨u, u_open, xu,_⟩,
id ┴ └────┘ └┘
src └─────┘ └┘ └┘ └─┘
typ └─────┘ ┴└┘└────┘└┘└┘└─┘
doc └─────┘ └┘ └┘ └─┘
txt └─────┘ └┘ └┘ └─┘
par └─────┘ └┘ └┘ └─┘
pid ┴ └┘ └┘ └─┘
st ───────────────────────────┘└─
551 apply differentiable_on.congr_mono (hu.2 m hm) (λy hy, _) (subset.refl _),
id └──────────────────────────┘ └┘ ┴ └┘ └─────────┘
src └────┘└──────────────────────────┘┴ └─┘ ┴ └┘ └───────┘ └─────────┘└─┘
typ └────┘└──────────────────────────┘┴ └┘└─┘┴┴└┘└┘ └───────┘ └─────────┘└─┘
doc └────┘ ┴ └─┘ ┴ └┘ └───────┘ └─┘
txt └────┘ ┴ └─┘ ┴ └┘ └───────┘ └─┘
par └────┘ ┴ └─┘ ┴ └┘ └───────┘ └─┘
pid ┴ ┴ └─┘ ┴ └┘ └───────┘ └─┘
st ────────────────────────────────────────────────────────────────────────────┘└─
552 symmetry,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
st ───────────┘└─
553 exact iterated_fderiv_within_inter_open hy.2 u_open hy.1 (hs.inter u_open) }
id └───────────────────────────────┘ └┘ └──────┘ └────┘
src └────┘└───────────────────────────────┘┴ └─┘ ┴ └─┘ └──────┘┴ └┘
typ └────┘└───────────────────────────────┘┴ └─┘ ┴└┘└─┘ └──────┘┴└────┘└┘
doc └────┘└───────────────────────────────┘┴ └─┘ ┴ └─┘ ┴ └┘
txt └────┘ ┴ └─┘ ┴ └─┘ ┴ └┘
par └────┘ ┴ └─┘ ┴ └─┘ ┴ └┘
pid ┴ ┴ └─┘ ┴ └─┘ ┴ ┴┴
st ──────────────────────────────────────────────────────────────────────────────┘└─
554 end
st ──┘
555
556 /--
557 A function is `C^n`, for `n : with_top ℕ`, if its derivatives of order at most `n` are all well
558 defined and continuous.
559 -/
560 def times_cont_diff (𝕜 : Type w) [nondiscrete_normed_field 𝕜] (n : with_top ℕ)
id └──────────────────────┘ ┴ └──────┘ ┴
src └──────────────────────┘ └──────┘ ┴
typ └──────────────────────┘ ┴ └──────┘ ┴
doc └──────────────────────┘
561 {E F : Type u} [normed_group E] [normed_space 𝕜 E]
id └──────────┘ ┴ └──────────┘ ┴ ┴
src └──────────┘ └──────────┘
typ └──────────┘ ┴ └──────────┘ ┴ ┴
doc └──────────┘ └──────────┘
562 [normed_group F] [normed_space 𝕜 F] (f : E → F) :=
id └──────────┘ ┴ └──────────┘ ┴ ┴ ┴ ┴
src └──────────┘ └──────────┘
typ └──────────┘ ┴ └──────────┘ ┴ ┴ ┴ ┴
doc └──────────┘ └──────────┘
563 (∀m:ℕ, (m : with_top ℕ) ≤ n → continuous (iterated_fderiv 𝕜 m f ))
id ┴ ┴ └──────┘ ┴ ┴ ┴ └────────┘ └─────────────┘ ┴ ┴ ┴
src ┴ └──────┘ ┴ ┴ └────────┘ └─────────────┘
typ ┴ ┴ └──────┘ ┴ ┴ ┴ └────────┘ └─────────────┘ ┴ ┴ ┴
doc └────────┘ └─────────────┘
564 ∧ (∀m:ℕ, (m : with_top ℕ) < n → differentiable 𝕜 (iterated_fderiv 𝕜 m f))
id ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ └────────────┘ ┴ └─────────────┘ ┴ ┴ ┴
src ┴ ┴ └──────┘ ┴ ┴ └────────────┘ └─────────────┘
typ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ └────────────┘ ┴ └─────────────┘ ┴ ┴ ┴
doc └────────────┘ └─────────────┘
565
566 lemma times_cont_diff_on_univ {n : with_top ℕ} :
id └──────┘ ┴
src └──────┘ ┴
typ └──────┘ ┴
567 times_cont_diff_on 𝕜 n f univ ↔ times_cont_diff 𝕜 n f :=
id └────────────────┘ ┴ ┴ ┴ └──┘ ┴ └─────────────┘ ┴ ┴ ┴
src └────────────────┘ └──┘ ┴ └─────────────┘
typ └────────────────┘ ┴ ┴ ┴ └──┘ ┴ └─────────────┘ ┴ ┴ ┴
doc └────────────────┘ └─────────────┘
568 by simp [times_cont_diff_on, times_cont_diff, iterated_fderiv_within_univ,
id └────────────────┘ └─────────────┘ └─────────────────────────┘
src └────┘└────────────────┘└┘└─────────────┘└┘└─────────────────────────┘└─
typ └────┘└────────────────┘└┘└─────────────┘└┘└─────────────────────────┘└─
doc └────┘└────────────────┘└┘└─────────────┘└┘ └─
txt └────┘ └┘ └┘ └─
par └────┘ └┘ └┘ └─
pid ┴┴ └┘ └┘ └─
st └────────────────────────────────────────────────────────────────────────
569 continuous_iff_continuous_on_univ, differentiable_on_univ]
id └───────────────────────────────┘ └────────────────────┘
src ───────┘└───────────────────────────────┘└┘└────────────────────┘└─
typ ───────┘└───────────────────────────────┘└┘└────────────────────┘└─
doc ───────┘ └┘ └─
txt ───────┘ └┘ └─
par ───────┘ └┘ └─
pid ───────┘ └┘ ┴└
st ───────────────────────────────────────────────────────────────────
570
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
571 @[simp] lemma times_cont_diff_zero :
doc └──┘
572 times_cont_diff 𝕜 0 f ↔ continuous f :=
id └─────────────┘ ┴ ┴ ┴ └────────┘ ┴
src └─────────────┘ ┴ └────────┘
typ └─────────────┘ ┴ ┴ ┴ └────────┘ ┴
doc └─────────────┘ └────────┘
573 by simp [times_cont_diff]
id └─────────────┘
src └────┘└─────────────┘└─
typ └────┘└─────────────┘└─
doc └────┘└─────────────┘└─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └───────────────────────
574
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
575 theorem times_cont_diff_iff_times_cont_diff_rec :
576 times_cont_diff 𝕜 n f ↔ times_cont_diff_rec 𝕜 n f :=
id └─────────────┘ ┴ ┴ ┴ ┴ └─────────────────┘ ┴ ┴ ┴
src └─────────────┘ ┴ └─────────────────┘
typ └─────────────┘ ┴ ┴ ┴ ┴ └─────────────────┘ ┴ ┴ ┴
doc └─────────────┘ └─────────────────┘
577 by simp [times_cont_diff_on_univ.symm, times_cont_diff_on_rec_univ.symm,
src └────┘ └┘ └─
typ └────┘└──────────────────────────┘└┘└──────────────────────────────┘└─
doc └────┘ └┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid ┴┴ └┘ └─
st └──────────────────────────────────────────────────────────────────────
578 times_cont_diff_on_iff_times_cont_diff_on_rec]
id └───────────────────────────────────────────┘
src ────────┘└───────────────────────────────────────────┘└─
typ ────────┘└───────────────────────────────────────────┘└─
doc ────────┘└───────────────────────────────────────────┘└─
txt ────────┘ └─
par ────────┘ └─
pid ────────┘ ┴└
st ────────────────────────────────────────────────────────
579
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
580 @[simp] lemma times_cont_diff_succ :
doc └──┘
581 times_cont_diff 𝕜 n.succ f ↔
id └─────────────┘ ┴ ┴└───┘ ┴ ┴
src └─────────────┘ └───┘ ┴
typ └─────────────┘ ┴ ┴└───┘ ┴ ┴
doc └─────────────┘
582 differentiable 𝕜 f ∧ times_cont_diff 𝕜 n (λx, fderiv 𝕜 f x) :=
id └────────────┘ ┴ ┴ ┴ └─────────────┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴
src └────────────┘ ┴ └─────────────┘ └────┘
typ └────────────┘ ┴ ┴ ┴ └─────────────┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴
doc └────────────┘ └─────────────┘ └────┘
583 by simp [times_cont_diff_iff_times_cont_diff_rec]
id └─────────────────────────────────────┘
src └────┘└─────────────────────────────────────┘└─
typ └────┘└─────────────────────────────────────┘└─
doc └────┘ └─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └───────────────────────────────────────────────
584
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
585 lemma times_cont_diff.of_le {m n : with_top ℕ} (h : times_cont_diff 𝕜 n f) (le : m ≤ n) :
id └──────┘ ┴ └─────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └──────┘ ┴ └─────────────┘ ┴
typ └──────┘ ┴ └─────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────────────┘
586 times_cont_diff 𝕜 m f :=
id └─────────────┘ ┴ ┴ ┴
src └─────────────┘
typ └─────────────┘ ┴ ┴ ┴
doc └─────────────┘
587 ⟨λp hp, h.1 p (le_trans hp le), λp hp, h.2 p (lt_of_lt_of_le hp le)⟩
id ┴ └┘ ┴┴ ┴ └──────┘ └┘ └┘ ┴ └┘ ┴┴ ┴ └────────────┘ └┘ └┘
src ┴ └──────┘ ┴ └────────────┘
typ ┴ └┘ ┴┴ ┴ └──────┘ └┘ └┘ ┴ └┘ ┴┴ ┴ └────────────┘ └┘ └┘
588
589 lemma times_cont_diff.of_succ (h : times_cont_diff 𝕜 n.succ f) : times_cont_diff 𝕜 n f :=
id └─────────────┘ ┴ ┴└───┘ ┴ └─────────────┘ ┴ ┴ ┴
src └─────────────┘ └───┘ └─────────────┘
typ └─────────────┘ ┴ ┴└───┘ ┴ └─────────────┘ ┴ ┴ ┴
doc └─────────────┘ └─────────────┘
590 h.of_le (with_top.coe_le_coe.2 (nat.le_succ n))
id ┴└────┘ └─────────────────┘┴ └─────────┘ ┴
src └────┘ └─────────────────┘┴ └─────────┘
typ ┴└────┘ └─────────────────┘┴ └─────────┘ ┴
591
592 lemma times_cont_diff.continuous {n : with_top ℕ} (h : times_cont_diff 𝕜 n f) :
id └──────┘ ┴ └─────────────┘ ┴ ┴ ┴
src └──────┘ ┴ └─────────────┘
typ └──────┘ ┴ └─────────────┘ ┴ ┴ ┴
doc └─────────────┘
593 continuous f :=
id └────────┘ ┴
src └────────┘
typ └────────┘ ┴
doc └────────┘
594 h.1 0 (by simp)
id ┴┴
src ┴ └──┘
typ ┴┴ └──┘
doc └──┘
txt └──┘
par └──┘
st └───┘
595
596 lemma times_cont_diff.continuous_fderiv {n : with_top ℕ} (h : times_cont_diff 𝕜 n f) (hn : 1 ≤ n) :
id └──────┘ ┴ └─────────────┘ ┴ ┴ ┴ ┴ ┴
src └──────┘ ┴ └─────────────┘ ┴
typ └──────┘ ┴ └─────────────┘ ┴ ┴ ┴ ┴ ┴
doc └─────────────┘
597 continuous (fderiv 𝕜 f) :=
id └────────┘ └────┘ ┴ ┴
src └────────┘ └────┘
typ └────────┘ └────┘ ┴ ┴
doc └────────┘ └────┘
598 h.1 1 hn
id ┴┴ └┘
src ┴
typ ┴┴ └┘
599
600 lemma times_cont_diff.continuous_fderiv_apply
601 {n : with_top ℕ} (h : times_cont_diff 𝕜 n f) (hn : 1 ≤ n) :
id └──────┘ ┴ └─────────────┘ ┴ ┴ ┴ ┴ ┴
src └──────┘ ┴ └─────────────┘ ┴
typ └──────┘ ┴ └─────────────┘ ┴ ┴ ┴ ┴ ┴
doc └─────────────┘
602 continuous (λp : E × E, (fderiv 𝕜 f p.1 : E → F) p.2) :=
id └────────┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴┴ ┴ ┴ ┴┴
src └────────┘ ┴ └────┘ ┴ ┴
typ └────────┘ ┴ ┴ ┴ └────┘ ┴ ┴ ┴┴ ┴ ┴ ┴┴
doc └────────┘ └────┘
603 begin
st └─────
604 have A : continuous (λq : (E →L[𝕜] F) × E, q.1 q.2) := is_bounded_bilinear_map_apply.continuous,
id └────────┘ └─┘┴┴ ┴ ┴ ┴ └──────────────────────────────────────┘
src └───────┘└────────┘┴ └──┘ ┴└─┘ ┴┴ └┘┴┴ └┘ └─┘ └─────┘└──────────────────────────────────────┘
typ └───────┘└────────┘┴ └──┘ ┴└─┘┴┴┴┴└┘┴┴┴└┘ └─┘ └─────┘└──────────────────────────────────────┘
doc └───────┘└────────┘┴ └──┘ ┴└─┘ ┴┴ └┘ ┴ └┘ └─┘ └─────┘
txt └───────┘ ┴ └──┘ ┴ ┴ └┘ ┴ └┘ └─┘ └─────┘
par └───────┘ ┴ └──┘ ┴ ┴ └┘ ┴ └┘ └─┘ └─────┘
pid └────┘└─┘ ┴ └──┘ ┴ ┴ └┘ ┴ └┘ └─┘ └─┘└──┘
st ────────────────────────────────────────────────────────────────────────────────────────────────┘└─
605 have B : continuous (λp : E × E, (fderiv 𝕜 f p.1, p.2)),
id └────────┘ ┴ ┴ ┴└────┘ ┴ ┴
src └───────┘└────────┘┴ └──┘ ┴ ┴ └┘┴└────┘┴ ┴ ┴ └──┘ └──┘
typ └───────┘└────────┘┴ └──┘ ┴┴┴┴└┘┴└────┘┴┴┴┴┴ └──┘ └──┘
doc └───────┘└────────┘┴ └──┘ ┴ ┴ └┘ └────┘┴ ┴ ┴ └──┘ └──┘
txt └───────┘ ┴ └──┘ ┴ ┴ └┘ ┴ ┴ ┴ └──┘ └──┘
par └───────┘ ┴ └──┘ ┴ ┴ └┘ ┴ ┴ ┴ └──┘ └──┘
pid └────┘└─┘ ┴ └──┘ ┴ ┴ └┘ ┴ ┴ ┴ └──┘ └──┘
st ────────────────────────────────────────────────────────┘└─
606 { apply continuous.prod_mk _ continuous_snd,
id └────────────────┘ └────────────┘
src └────┘└────────────────┘└─┘└────────────┘
typ └────┘└────────────────┘└─┘└────────────┘
doc └────┘ └─┘
txt └────┘ └─┘
par └────┘ └─┘
pid ┴ └─┘
st ───┘└───────────────────────────────────────┘└─
607 exact continuous.comp (h.continuous_fderiv hn) continuous_fst },
id └─────────────┘ └─────────────────┘ └┘ └────────────┘
src └────┘└─────────────┘┴ └─────────────────┘┴ └┘└────────────┘┴
typ └────┘└─────────────┘┴ └─────────────────┘┴└┘└┘└────────────┘┴
doc └────┘ ┴ ┴ └┘ ┴
txt └────┘ ┴ ┴ └┘ ┴
par └────┘ ┴ ┴ └┘ ┴
pid ┴ ┴ ┴ └┘ ┴
st ─────────────────────────────────────────────────────────────────┘└┘└
608 exact A.comp B
id └────┘ ┴
src └────┘└────┘┴ ┴
typ └────┘└────┘┴┴┴
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ────────────────┘
609 end
st └─┘
610
611 lemma times_cont_diff_top : times_cont_diff 𝕜 ⊤ f ↔ (∀n:ℕ, times_cont_diff 𝕜 n f) :=
id └─────────────┘ ┴ ┴ ┴ ┴ ┴ └─────────────┘ ┴ ┴ ┴
src └─────────────┘ ┴ ┴ ┴ └─────────────┘
typ └─────────────┘ ┴ ┴ ┴ ┴ ┴ └─────────────┘ ┴ ┴ ┴
doc └─────────────┘ └─────────────┘
612 by simp [times_cont_diff_on_univ.symm, times_cont_diff_on_rec_univ.symm,
src └────┘ └┘ └─
typ └────┘└──────────────────────────┘└┘└──────────────────────────────┘└─
doc └────┘ └┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid ┴┴ └┘ └─
st └──────────────────────────────────────────────────────────────────────
613 times_cont_diff_on_top]
id └────────────────────┘
src ───────┘└────────────────────┘└─
typ ───────┘└────────────────────┘└─
doc ───────┘ └─
txt ───────┘ └─
par ───────┘ └─
pid ───────┘ ┴└
st ────────────────────────────────
614
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
615 lemma times_cont_diff.times_cont_diff_on {n : with_top ℕ} {s : set E}
id └──────┘ ┴ └─┘ ┴
src └──────┘ ┴ └─┘
typ └──────┘ ┴ └─┘ ┴
616 (h : times_cont_diff 𝕜 n f) (hs : unique_diff_on 𝕜 s) : times_cont_diff_on 𝕜 n f s :=
id └─────────────┘ ┴ ┴ ┴ └────────────┘ ┴ ┴ └────────────────┘ ┴ ┴ ┴ ┴
src └─────────────┘ └────────────┘ └────────────────┘
typ └─────────────┘ ┴ ┴ ┴ └────────────┘ ┴ ┴ └────────────────┘ ┴ ┴ ┴ ┴
doc └─────────────┘ └────────────┘ └────────────────┘
617 by { rw ← times_cont_diff_on_univ at h, apply times_cont_diff_on.mono h (subset_univ _) hs }
id └─────────────────────┘ └─────────────────────┘ ┴ └─────────┘ └┘
src └───┘└─────────────────────┘└───┘ └────┘└─────────────────────┘┴ ┴ └─────────┘└──┘ ┴
typ └───┘└─────────────────────┘└───┘ └────┘└─────────────────────┘┴┴┴ └─────────┘└──┘└┘┴
doc └───┘ └───┘ └────┘ ┴ ┴ └──┘ ┴
txt └───┘ └───┘ └────┘ ┴ ┴ └──┘ ┴
par └───┘ └───┘ └────┘ ┴ ┴ └──┘ ┴
pid └─┘ └───┘ ┴ ┴ ┴ └──┘ ┴
st └──────────────────────────────────┘└───────────────────────────────────────────────────┘└┘
618
619 /--
620 Constants are C^∞.
621 -/
622 lemma times_cont_diff_const {n : with_top ℕ} {c : F} : times_cont_diff 𝕜 n (λx : E, c) :=
id └──────┘ ┴ ┴ └─────────────┘ ┴ ┴ ┴ ┴
src └──────┘ ┴ └─────────────┘
typ └──────┘ ┴ ┴ └─────────────┘ ┴ ┴ ┴ ┴
doc └─────────────┘
623 begin
st └─────
624 tactic.unfreeze_local_instances,
id └─────────────────────────────┘
src └─────────────────────────────┘
typ └─────────────────────────────┘
doc └─────────────────────────────┘
par └─────────────────────────────┘
st ───────────────────────────────────
625 induction n using with_top.nat_induction with n IH Itop generalizing F,
id ┴
src └────────┘ └─────────────────────────────────────────────────────────┘
typ └────────┘┴└─────────────────────────────────────────────────────────┘
doc └────────┘ └─────────────────────────────────────────────────────────┘
txt └────────┘ └─────────────────────────────────────────────────────────┘
par └────────┘ └─────────────────────────────────────────────────────────┘
pid ┴ └───────────────────────────┘└─────────────┘└─────────────┘
st ───────────────────────────────────────────────────────────────────────┘└─
626 { rw times_cont_diff_zero,
id └──────────────────┘
src └─┘└──────────────────┘
typ └─┘└──────────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ───┘└─────────────────────┘└─
627 apply continuous_const },
id └──────────────┘
src └────┘└──────────────┘┴
typ └────┘└──────────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ──────────────────────────┘└┘└
628 { refine times_cont_diff_succ.2 ⟨differentiable_const _, _⟩,
id └──────────────────┘ └──────────────────┘
src └─────┘└──────────────────┘└─┘ └──────────────────┘└────┘
typ └─────┘└──────────────────┘└─┘ └──────────────────┘└────┘
doc └─────┘ └─┘ └────┘
txt └─────┘ └─┘ └────┘
par └─────┘ └─┘ └────┘
pid ┴ └─┘ └────┘
st ───┘└───────────────────────────────────────────────────────┘└─
629 simp [fderiv_const],
id └──────────┘
src └────┘└──────────┘┴
typ └────┘└──────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st ──────────────────────┘└─
630 exact IH },
id └┘
src └────┘ ┴
typ └────┘└┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ────────────┘└┘└
631 { rw times_cont_diff_top,
id └─────────────────┘
src └─┘└─────────────────┘
typ └─┘└─────────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ─────────────────────────┘└─
632 assume n, apply Itop }
src └──────┘ └────┘ ┴
typ └──────┘ └────┘ ┴
doc └──────┘ └────┘ ┴
txt └──────┘ └────┘ ┴
par └──────┘ └────┘ ┴
pid └──────┘ ┴ ┴
st ───────────┘└───────────┘└─
633 end
st ──┘
634
635 lemma times_cont_diff_on_const {n : with_top ℕ} {c : F} {s : set E} (hs : unique_diff_on 𝕜 s) :
id └──────┘ ┴ ┴ └─┘ ┴ └────────────┘ ┴ ┴
src └──────┘ ┴ └─┘ └────────────┘
typ └──────┘ ┴ ┴ └─┘ ┴ └────────────┘ ┴ ┴
doc └────────────┘
636 times_cont_diff_on 𝕜 n (λx : E, c) s :=
id └────────────────┘ ┴ ┴ ┴ ┴ ┴
src └────────────────┘
typ └────────────────┘ ┴ ┴ ┴ ┴ ┴
doc └────────────────┘
637 times_cont_diff_const.times_cont_diff_on hs
id └───────────────────┘└─────────────────┘ └┘
src └───────────────────┘└─────────────────┘
typ └───────────────────┘└─────────────────┘ └┘
doc └───────────────────┘
638
639 /--
640 Linear functions are C^∞.
641 -/
642 lemma is_bounded_linear_map.times_cont_diff {n : with_top ℕ} (hf : is_bounded_linear_map 𝕜 f) :
id └──────┘ ┴ └───────────────────┘ ┴ ┴
src └──────┘ ┴ └───────────────────┘
typ └──────┘ ┴ └───────────────────┘ ┴ ┴
doc └───────────────────┘
643 times_cont_diff 𝕜 n f :=
id └─────────────┘ ┴ ┴ ┴
src └─────────────┘
typ └─────────────┘ ┴ ┴ ┴
doc └─────────────┘
644 begin
st └─────
645 induction n using with_top.nat_induction with n IH Itop,
id ┴
src └────────┘ └──────────────────────────────────────────┘
typ └────────┘┴└──────────────────────────────────────────┘
doc └────────┘ └──────────────────────────────────────────┘
txt └────────┘ └──────────────────────────────────────────┘
par └────────┘ └──────────────────────────────────────────┘
pid ┴ └───────────────────────────┘└─────────────┘
st ────────────────────────────────────────────────────────┘└─
646 { rw times_cont_diff_zero,
id └──────────────────┘
src └─┘└──────────────────┘
typ └─┘└──────────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ───┘└─────────────────────┘└─
647 exact hf.continuous },
id └───────────┘
src └────┘└───────────┘┴
typ └────┘└───────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───────────────────────┘└┘└
648 { refine times_cont_diff_succ.2 ⟨hf.differentiable, _⟩,
id └──────────────────┘ └───────────────┘
src └─────┘└──────────────────┘└─┘ └───────────────┘└──┘
typ └─────┘└──────────────────┘└─┘ └───────────────┘└──┘
doc └─────┘ └─┘ └──┘
txt └─────┘ └─┘ └──┘
par └─────┘ └─┘ └──┘
pid ┴ └─┘ └──┘
st ───┘└──────────────────────────────────────────────────┘└─
649 simp [hf.fderiv],
src └────┘ ┴
typ └────┘└───────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st ───────────────────┘└─
650 exact times_cont_diff_const },
id └───────────────────┘
src └────┘└───────────────────┘┴
typ └────┘└───────────────────┘┴
doc └────┘└───────────────────┘┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───────────────────────────────┘└┘└
651 { rw times_cont_diff_top, apply Itop }
id └─────────────────┘
src └─┘└─────────────────┘ └────┘ ┴
typ └─┘└─────────────────┘ └────┘ ┴
doc └─┘ └────┘ ┴
txt └─┘ └────┘ ┴
par └─┘ └────┘ ┴
pid ┴ ┴ ┴
st ─────────────────────────┘└───────────┘└─
652 end
st ──┘
653
654 /--
655 The first projection in a product is C^∞.
656 -/
657 lemma times_cont_diff_fst {n : with_top ℕ} : times_cont_diff 𝕜 n (prod.fst : E × F → E) :=
id └──────┘ ┴ └─────────────┘ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴
src └──────┘ ┴ └─────────────┘ └──────┘ ┴
typ └──────┘ ┴ └─────────────┘ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴
doc └─────────────┘
658 is_bounded_linear_map.times_cont_diff is_bounded_linear_map.fst
id └───────────────────────────────────┘ └───────────────────────┘
src └───────────────────────────────────┘ └───────────────────────┘
typ └───────────────────────────────────┘ └───────────────────────┘
doc └───────────────────────────────────┘
659
660 /--
661 The second projection in a product is C^∞.
662 -/
663 lemma times_cont_diff_snd {n : with_top ℕ} : times_cont_diff 𝕜 n (prod.snd : E × F → F) :=
id └──────┘ ┴ └─────────────┘ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴
src └──────┘ ┴ └─────────────┘ └──────┘ ┴
typ └──────┘ ┴ └─────────────┘ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴
doc └─────────────┘
664 is_bounded_linear_map.times_cont_diff is_bounded_linear_map.snd
id └───────────────────────────────────┘ └───────────────────────┘
src └───────────────────────────────────┘ └───────────────────────┘
typ └───────────────────────────────────┘ └───────────────────────┘
doc └───────────────────────────────────┘
665
666 /--
667 The identity is C^∞.
668 -/
669 lemma times_cont_diff_id {n : with_top ℕ} : times_cont_diff 𝕜 n (id : E → E) :=
id └──────┘ ┴ └─────────────┘ ┴ ┴ └┘ ┴ ┴
src └──────┘ ┴ └─────────────┘ └┘
typ └──────┘ ┴ └─────────────┘ ┴ ┴ └┘ ┴ ┴
doc └─────────────┘
670 is_bounded_linear_map.id.times_cont_diff
id └──────────────────────┘└──────────────┘
src └──────────────────────┘└──────────────┘
typ └──────────────────────┘└──────────────┘
doc └──────────────┘
671
672 /--
673 Bilinear functions are C^∞.
674 -/
675 lemma is_bounded_bilinear_map.times_cont_diff {n : with_top ℕ} (hb : is_bounded_bilinear_map 𝕜 b) :
id └──────┘ ┴ └─────────────────────┘ ┴ ┴
src └──────┘ ┴ └─────────────────────┘
typ └──────┘ ┴ └─────────────────────┘ ┴ ┴
doc └─────────────────────┘
676 times_cont_diff 𝕜 n b :=
id └─────────────┘ ┴ ┴ ┴
src └─────────────┘
typ └─────────────┘ ┴ ┴ ┴
doc └─────────────┘
677 begin
st └─────
678 induction n using with_top.nat_induction with n IH Itop,
id ┴
src └────────┘ └──────────────────────────────────────────┘
typ └────────┘┴└──────────────────────────────────────────┘
doc └────────┘ └──────────────────────────────────────────┘
txt └────────┘ └──────────────────────────────────────────┘
par └────────┘ └──────────────────────────────────────────┘
pid ┴ └───────────────────────────┘└─────────────┘
st ────────────────────────────────────────────────────────┘└─
679 { rw times_cont_diff_zero,
id └──────────────────┘
src └─┘└──────────────────┘
typ └─┘└──────────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ───┘└─────────────────────┘└─
680 exact hb.continuous },
id └───────────┘
src └────┘└───────────┘┴
typ └────┘└───────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───────────────────────┘└┘└
681 { refine times_cont_diff_succ.2 ⟨hb.differentiable, _⟩,
id └──────────────────┘ └───────────────┘
src └─────┘└──────────────────┘└─┘ └───────────────┘└──┘
typ └─────┘└──────────────────┘└─┘ └───────────────┘└──┘
doc └─────┘ └─┘ └──┘
txt └─────┘ └─┘ └──┘
par └─────┘ └─┘ └──┘
pid ┴ └─┘ └──┘
st ───┘└──────────────────────────────────────────────────┘└─
682 simp [hb.fderiv],
src └────┘ ┴
typ └────┘└───────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴┴ ┴
st ───────────────────┘└─
683 exact hb.is_bounded_linear_map_deriv.times_cont_diff },
id └────────────────────────────────────────────┘
src └────┘└────────────────────────────────────────────┘┴
typ └────┘└────────────────────────────────────────────┘┴
doc └────┘└────────────────────────────────────────────┘┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ────────────────────────────────────────────────────────┘└┘└
684 { rw times_cont_diff_top, apply Itop }
id └─────────────────┘
src └─┘└─────────────────┘ └────┘ ┴
typ └─┘└─────────────────┘ └────┘ ┴
doc └─┘ └────┘ ┴
txt └─┘ └────┘ ┴
par └─┘ └────┘ ┴
pid ┴ ┴ ┴
st ─────────────────────────┘└───────────┘└─
685 end
st ──┘
686
687 /--
688 Composition by bounded linear maps preserves `C^n` functions on domains.
689 -/
690 lemma times_cont_diff_on.comp_is_bounded_linear {n : with_top ℕ} {s : set E} {f : E → F} {g : F → G}
id └──────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴
src └──────┘ ┴ └─┘
typ └──────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴
691 (hf : times_cont_diff_on 𝕜 n f s) (hg : is_bounded_linear_map 𝕜 g) (hs : unique_diff_on 𝕜 s) :
id └────────────────┘ ┴ ┴ ┴ ┴ └───────────────────┘ ┴ ┴ └────────────┘ ┴ ┴
src └────────────────┘ └───────────────────┘ └────────────┘
typ └────────────────┘ ┴ ┴ ┴ ┴ └───────────────────┘ ┴ ┴ └────────────┘ ┴ ┴
doc └────────────────┘ └───────────────────┘ └────────────┘
692 times_cont_diff_on 𝕜 n (λx, g (f x)) s :=
id └────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └────────────────┘
typ └────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └────────────────┘
693 begin
st └─────
694 tactic.unfreeze_local_instances,
id └─────────────────────────────┘
src └─────────────────────────────┘
typ └─────────────────────────────┘
doc └─────────────────────────────┘
par └─────────────────────────────┘
st ───────────────────────────────────
695 induction n using with_top.nat_induction with n IH Itop generalizing F G,
id ┴
src └────────┘ └───────────────────────────────────────────────────────────┘
typ └────────┘┴└───────────────────────────────────────────────────────────┘
doc └────────┘ └───────────────────────────────────────────────────────────┘
txt └────────┘ └───────────────────────────────────────────────────────────┘
par └────────┘ └───────────────────────────────────────────────────────────┘
pid ┴ └───────────────────────────┘└─────────────┘└───────────────┘
st ─────────────────────────────────────────────────────────────────────────┘└─
696 { have : continuous_on g univ := hg.continuous.continuous_on,
id └───────────┘ ┴ └──┘ └─────────────────────────┘
src └─────┘└───────────┘┴ ┴└──┘└──┘└─────────────────────────┘
typ └─────┘└───────────┘┴┴┴└──┘└──┘└─────────────────────────┘
doc └─────┘└───────────┘┴ ┴ └──┘
txt └─────┘ ┴ ┴ └──┘
par └─────┘ ┴ ┴ └──┘
pid └───┘└┘ ┴ ┴ └──┘
st ───┘└────────────────────────────────────────────────────────┘└─
697 rw times_cont_diff_on_zero at hf ⊢,
id └─────────────────────┘
src └─┘└─────────────────────┘└──────┘
typ └─┘└─────────────────────┘└──────┘
doc └─┘ └──────┘
txt └─┘ └──────┘
par └─┘ └──────┘
pid ┴ └──────┘
st ─────────────────────────────────────┘└─
698 apply continuous_on.comp this hf (subset_univ _) },
id └────────────────┘ └──┘ └┘ └─────────┘
src └────┘└────────────────┘┴ ┴ ┴ └─────────┘└──┘
typ └────┘└────────────────┘┴└──┘┴└┘┴ └─────────┘└──┘
doc └────┘ ┴ ┴ ┴ └──┘
txt └────┘ ┴ ┴ ┴ └──┘
par └────┘ ┴ ┴ ┴ └──┘
pid ┴ ┴ ┴ ┴ └─┘┴
st ────────────────────────────────────────────────────┘└┘└
699 { rw times_cont_diff_on_succ at hf ⊢,
id └─────────────────────┘
src └─┘└─────────────────────┘└──────┘
typ └─┘└─────────────────────┘└──────┘
doc └─┘ └──────┘
txt └─┘ └──────┘
par └─┘ └──────┘
pid ┴ └──────┘
st ───┘└────────────────────────────────┘└─
700 refine ⟨differentiable_on.comp hg.differentiable_on hf.1 subset_preimage_univ, _⟩,
id └────────────────────┘ └──────────────────┘ └┘ └──────────────────┘
src └─────┘ └────────────────────┘┴└──────────────────┘┴ └─┘└──────────────────┘└──┘
typ └─────┘ └────────────────────┘┴└──────────────────┘┴└┘└─┘└──────────────────┘└──┘
doc └─────┘ ┴ ┴ └─┘ └──┘
txt └─────┘ ┴ ┴ └─┘ └──┘
par └─────┘ ┴ ┴ └─┘ └──┘
pid ┴ ┴ ┴ └─┘ └──┘
st ────────────────────────────────────────────────────────────────────────────────────┘└─
701 let Φ : (E →L[𝕜] F) → (E →L[𝕜] G) := λu, continuous_linear_map.comp (hg.to_continuous_linear_map) u,
id └─┘ ┴ ┴ ┴ ┴ ┴ └────────────────────────┘ └─────────────────────────┘
src └──────┘ ┴└─┘ ┴┴ └┘ ┴ ┴ ┴ └───┘ └─┘└────────────────────────┘┴ └─────────────────────────┘└┘
typ └──────┘ ┴└─┘ ┴┴┴└┘ ┴ ┴┴ ┴ ┴┴└───┘ └─┘└────────────────────────┘┴ └─────────────────────────┘└┘
doc └──────┘ ┴└─┘ ┴┴ └┘ ┴ ┴ ┴ └───┘ └─┘└────────────────────────┘┴ └─────────────────────────┘└┘
txt └──────┘ ┴ ┴ └┘ ┴ ┴ ┴ └───┘ └─┘ ┴ └┘
par └──────┘ ┴ ┴ └┘ ┴ ┴ ┴ └───┘ └─┘ ┴ └┘
pid └───┘└─┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴└──┘ └─┘ ┴ └┘
st ──────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
702 have : ∀x∈s, fderiv_within 𝕜 (g ∘ f) s x = Φ (fderiv_within 𝕜 f s x),
id ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴
src └─────┘ └┘ ┴ ┴ ┴ ┴┴┴ └┘ ┴ ┴┴┴ ┴ └───────────┘┴ ┴ ┴ ┴ ┴
typ └─────┘ └┘ ┴ ┴ ┴ ┴┴┴┴ └┘ ┴ ┴┴┴┴┴ └───────────┘┴┴┴┴┴┴┴ ┴
doc └─────┘ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └───────────┘┴ ┴ ┴ ┴ ┴
txt └─────┘ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par └─────┘ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid └───┘└┘ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ───────────────────────────────────────────────────────────────────────┘└─
703 { assume x hx,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────────┘
st ─────┘└─────────┘└─
704 rw [fderiv_within.comp x _ (hf.1 x hx) subset_preimage_univ (hs x hx),
id └────────────────┘ └┘ └──────────────────┘ └┘ ┴ └┘
src └──┘└────────────────┘┴ └─┘ └─┘ ┴ └┘└──────────────────┘┴ ┴ ┴ └──
typ └──┘└────────────────┘┴ └─┘ └┘└─┘ ┴ └┘└──────────────────┘┴ └┘┴┴┴└┘└──
doc └──┘ ┴ └─┘ └─┘ ┴ └┘ ┴ ┴ ┴ └──
txt └──┘ ┴ └─┘ └─┘ ┴ └┘ ┴ ┴ ┴ └──
par └──┘ ┴ └─┘ └─┘ ┴ └┘ ┴ ┴ ┴ └──
pid └┘ ┴ └─┘ └─┘ ┴ └┘ ┴ ┴ ┴ └──
st ──────────────────────────────────────────────────────────────────────────┘└─
705 fderiv_within_univ, hg.fderiv],
id └────────────────┘
src ─────────┘└────────────────┘└┘ ┴
typ ─────────┘└────────────────┘└┘└───────┘┴
doc ─────────┘ └┘ ┴
txt ─────────┘ └┘ ┴
par ─────────┘ └┘ ┴
pid ─────────┘ └┘ ┴
st ───────────────────────────┘└─────────┘└──
706 rw differentiable_within_at_univ,
id └───────────────────────────┘
src └─┘└───────────────────────────┘
typ └─┘└───────────────────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ─────────────────────────────────────┘└─
707 exact hg.differentiable_at },
id └──────────────────┘
src └────┘└──────────────────┘┴
typ └────┘└──────────────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ────────────────────────────────┘└┘└
708 apply times_cont_diff_on.congr_mono _ hs this (subset.refl _),
id └───────────────────────────┘ └┘ └──┘ └─────────┘
src └────┘└───────────────────────────┘└─┘ ┴ ┴ └─────────┘└─┘
typ └────┘└───────────────────────────┘└─┘└┘┴└──┘┴ └─────────┘└─┘
doc └────┘ └─┘ ┴ ┴ └─┘
txt └────┘ └─┘ ┴ ┴ └─┘
par └────┘ └─┘ ┴ ┴ └─┘
pid ┴ └─┘ ┴ ┴ └─┘
st ────────────────────────────────────────────────────────────────┘└─
709 simp only [times_cont_diff_on_succ] at hf,
id └─────────────────────┘
src └─────────┘└─────────────────────┘└─────┘
typ └─────────┘└─────────────────────┘└─────┘
doc └─────────┘ └─────┘
txt └─────────┘ └─────┘
par └─────────┘ └─────┘
pid ┴└──┘└┘ ┴┴└───┘
st ────────────────────────────────────────────┘└─
710 exact IH hf.2 hg.to_continuous_linear_map.is_bounded_linear_map_comp_left },
id └┘ └┘ └─────────────────────────────────────────────────────────┘
src └────┘ ┴ └─┘└─────────────────────────────────────────────────────────┘┴
typ └────┘└┘┴└┘└─┘└─────────────────────────────────────────────────────────┘┴
doc └────┘ ┴ └─┘└─────────────────────────────────────────────────────────┘┴
txt └────┘ ┴ └─┘ ┴
par └────┘ ┴ └─┘ ┴
pid ┴ ┴ └─┘ ┴
st ─────────────────────────────────────────────────────────────────────────────┘└┘└
711 { rw times_cont_diff_on_top at hf ⊢,
id └────────────────────┘
src └─┘└────────────────────┘└──────┘
typ └─┘└────────────────────┘└──────┘
doc └─┘ └──────┘
txt └─┘ └──────┘
par └─┘ └──────┘
pid ┴ └──────┘
st ────────────────────────────────────┘└─
712 assume n,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ───────────┘└─
713 apply Itop n (hf n) hg }
id └──┘ └┘ ┴ └┘
src └────┘ ┴ ┴ ┴ └┘ ┴
typ └────┘└──┘┴ ┴ └┘┴┴└┘└┘┴
doc └────┘ ┴ ┴ ┴ └┘ ┴
txt └────┘ ┴ ┴ ┴ └┘ ┴
par └────┘ ┴ ┴ ┴ └┘ ┴
pid ┴ ┴ ┴ ┴ └┘ ┴
st ──────────────────────────┘└─
714 end
st ──┘
715
716 /--
717 Composition by bounded linear maps preserves `C^n` functions.
718 -/
719 lemma times_cont_diff.comp_is_bounded_linear {n : with_top ℕ} {f : E → F} {g : F → G}
id └──────┘ ┴ ┴ ┴ ┴ ┴
src └──────┘ ┴
typ └──────┘ ┴ ┴ ┴ ┴ ┴
720 (hf : times_cont_diff 𝕜 n f) (hg : is_bounded_linear_map 𝕜 g) :
id └─────────────┘ ┴ ┴ ┴ └───────────────────┘ ┴ ┴
src └─────────────┘ └───────────────────┘
typ └─────────────┘ ┴ ┴ ┴ └───────────────────┘ ┴ ┴
doc └─────────────┘ └───────────────────┘
721 times_cont_diff 𝕜 n (λx, g (f x)) :=
id └─────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └─────────────┘
typ └─────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────────────┘
722 times_cont_diff_on_univ.1 $ times_cont_diff_on.comp_is_bounded_linear (times_cont_diff_on_univ.2 hf)
id └─────────────────────┘┴ └───────────────────────────────────────┘ └─────────────────────┘┴ └┘
src └─────────────────────┘┴ └───────────────────────────────────────┘ └─────────────────────┘┴
typ └─────────────────────┘┴ └───────────────────────────────────────┘ └─────────────────────┘┴ └┘
doc └───────────────────────────────────────┘
723 hg is_open_univ.unique_diff_on
id └┘ └──────────┘└─────────────┘
src └──────────┘└─────────────┘
typ └┘ └──────────┘└─────────────┘
724
725 /--
726 The cartesian product of `C^n` functions on domains is `C^n`.
727 -/
728 lemma times_cont_diff_on.prod {n : with_top ℕ} {s : set E} {f : E → F} {g : E → G}
id └──────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴
src └──────┘ ┴ └─┘
typ └──────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴
729 (hf : times_cont_diff_on 𝕜 n f s) (hg : times_cont_diff_on 𝕜 n g s) (hs : unique_diff_on 𝕜 s) :
id └────────────────┘ ┴ ┴ ┴ ┴ └────────────────┘ ┴ ┴ ┴ ┴ └────────────┘ ┴ ┴
src └────────────────┘ └────────────────┘ └────────────┘
typ └────────────────┘ ┴ ┴ ┴ ┴ └────────────────┘ ┴ ┴ ┴ ┴ └────────────┘ ┴ ┴
doc └────────────────┘ └────────────────┘ └────────────┘
730 times_cont_diff_on 𝕜 n (λx:E, (f x, g x)) s :=
id └────────────────┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
src └────────────────┘ ┴
typ └────────────────┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
doc └────────────────┘
731 begin
st └─────
732 tactic.unfreeze_local_instances,
id └─────────────────────────────┘
src └─────────────────────────────┘
typ └─────────────────────────────┘
doc └─────────────────────────────┘
par └─────────────────────────────┘
st ───────────────────────────────────
733 induction n using with_top.nat_induction with n IH Itop generalizing F G,
id ┴
src └────────┘ └───────────────────────────────────────────────────────────┘
typ └────────┘┴└───────────────────────────────────────────────────────────┘
doc └────────┘ └───────────────────────────────────────────────────────────┘
txt └────────┘ └───────────────────────────────────────────────────────────┘
par └────────┘ └───────────────────────────────────────────────────────────┘
pid ┴ └───────────────────────────┘└─────────────┘└───────────────┘
st ─────────────────────────────────────────────────────────────────────────┘└─
734 { rw times_cont_diff_on_zero at hf hg ⊢,
id └─────────────────────┘
src └─┘└─────────────────────┘└─────────┘
typ └─┘└─────────────────────┘└─────────┘
doc └─┘ └─────────┘
txt └─┘ └─────────┘
par └─┘ └─────────┘
pid ┴ └─────────┘
st ───┘└───────────────────────────────────┘└─
735 exact continuous_on.prod hf hg },
id └────────────────┘ └┘ └┘
src └────┘└────────────────┘┴ ┴ ┴
typ └────┘└────────────────┘┴└┘┴└┘┴
doc └────┘ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ──────────────────────────────────┘└┘└
736 { rw times_cont_diff_on_succ at hf hg ⊢,
id └─────────────────────┘
src └─┘└─────────────────────┘└─────────┘
typ └─┘└─────────────────────┘└─────────┘
doc └─┘ └─────────┘
txt └─┘ └─────────┘
par └─┘ └─────────┘
pid ┴ └─────────┘
st ───┘└───────────────────────────────────┘└─
737 refine ⟨differentiable_on.prod hf.1 hg.1, _⟩,
id └────────────────────┘ └┘ └┘
src └─────┘ └────────────────────┘┴ └─┘ └────┘
typ └─────┘ └────────────────────┘┴└┘└─┘└┘└────┘
doc └─────┘ ┴ └─┘ └────┘
txt └─────┘ ┴ └─┘ └────┘
par └─────┘ ┴ └─┘ └────┘
pid ┴ ┴ └─┘ └────┘
st ───────────────────────────────────────────────┘└─
738 let F₁ := λx : E, (fderiv_within 𝕜 f s x, fderiv_within 𝕜 g s x),
id ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴
src └────────┘ └──┘ └┘┴ ┴ ┴ ┴ ┴ └┘└───────────┘┴ ┴ ┴ ┴ ┴
typ └────────┘ └──┘┴└┘┴ ┴ ┴┴┴ ┴ └┘└───────────┘┴┴┴┴┴┴┴ ┴
doc └────────┘ └──┘ └┘ ┴ ┴ ┴ ┴ └┘└───────────┘┴ ┴ ┴ ┴ ┴
txt └────────┘ └──┘ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴
par └────────┘ └──┘ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴
pid └────┘┴└─┘ └──┘ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴
st ───────────────────────────────────────────────────────────────────┘└─
739 let Φ : ((E →L[𝕜] F) × (E →L[𝕜] G)) → (E →L[𝕜] (F × G)) := λp, continuous_linear_map.prod p.1 p.2,
id └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └────────────────────────┘
src └──────┘ ┴└─┘ ┴┴ └┘┴┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └────┘ └─┘└────────────────────────┘┴ └─┘ └┘
typ └──────┘ ┴└─┘ ┴┴ └┘┴┴ ┴ ┴ └─┘ ┴ ┴┴ ┴ ┴ ┴┴ ┴┴└────┘ └─┘└────────────────────────┘┴ └─┘ └┘
doc └──────┘ ┴└─┘ ┴┴ └┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └────┘ └─┘└────────────────────────┘┴ └─┘ └┘
txt └──────┘ ┴ ┴ └┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └────┘ └─┘ ┴ └─┘ └┘
par └──────┘ ┴ ┴ └┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └────┘ └─┘ ┴ └─┘ └┘
pid └───┘└─┘ ┴ ┴ └┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └┘└──┘ └─┘ ┴ └─┘ └┘
st ────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
740 have : times_cont_diff_on 𝕜 n (Φ ∘ F₁) s :=
id └────────────────┘ ┴ ┴ ┴ ┴ └┘ ┴
src └─────┘└────────────────┘┴ ┴ ┴ ┴┴┴ └┘ └───
typ └─────┘└────────────────┘┴┴┴┴┴ ┴┴┴┴└┘└┘┴└───
doc └─────┘└────────────────┘┴ ┴ ┴ ┴ ┴ └┘ └───
txt └─────┘ ┴ ┴ ┴ ┴ ┴ └┘ └───
par └─────┘ ┴ ┴ ┴ ┴ ┴ └┘ └───
pid └───┘└┘ ┴ ┴ ┴ ┴ ┴ └┘ └───
st ────────────────────────────────────────────────
741 times_cont_diff_on.comp_is_bounded_linear (IH hf.2 hg.2) is_bounded_linear_map_prod_iso hs,
id └───────────────────────────────────────┘ └┘ └┘ └┘ └────────────────────────────┘ └┘
src ─────┘└───────────────────────────────────────┘┴ ┴ └─┘ └──┘└────────────────────────────┘┴
typ ─────┘└───────────────────────────────────────┘┴ └┘┴└┘└─┘└┘└──┘└────────────────────────────┘┴└┘
doc ─────┘└───────────────────────────────────────┘┴ ┴ └─┘ └──┘ ┴
txt ─────┘ ┴ ┴ └─┘ └──┘ ┴
par ─────┘ ┴ ┴ └─┘ └──┘ ┴
pid ─────┘ ┴ ┴ └─┘ └──┘ ┴
st ───────────────────────────────────────────────────────────────────────────────────────────────┘└─
742 apply times_cont_diff_on.congr_mono this hs (λx hx, _) (subset.refl _),
id └───────────────────────────┘ └──┘ └┘ └─────────┘
src └────┘└───────────────────────────┘┴ ┴ ┴ └───────┘ └─────────┘└─┘
typ └────┘└───────────────────────────┘┴└──┘┴└┘┴ └───────┘ └─────────┘└─┘
doc └────┘ ┴ ┴ ┴ └───────┘ └─┘
txt └────┘ ┴ ┴ ┴ └───────┘ └─┘
par └────┘ ┴ ┴ ┴ └───────┘ └─┘
pid ┴ ┴ ┴ ┴ └───────┘ └─┘
st ─────────────────────────────────────────────────────────────────────────┘└─
743 apply differentiable_at.fderiv_within_prod (hf.1 x hx) (hg.1 x hx) (hs x hx) },
id └──────────────────────────────────┘ └┘ └┘ └┘ ┴ └┘
src └────┘└──────────────────────────────────┘┴ └─┘ ┴ └┘ └─┘ ┴ └┘ ┴ ┴ └┘
typ └────┘└──────────────────────────────────┘┴ └┘└─┘ ┴ └┘ └┘└─┘ ┴ └┘ └┘┴┴┴└┘└┘
doc └────┘ ┴ └─┘ ┴ └┘ └─┘ ┴ └┘ ┴ ┴ └┘
txt └────┘ ┴ └─┘ ┴ └┘ └─┘ ┴ └┘ ┴ ┴ └┘
par └────┘ ┴ └─┘ ┴ └┘ └─┘ ┴ └┘ ┴ ┴ └┘
pid ┴ ┴ └─┘ ┴ └┘ └─┘ ┴ └┘ ┴ ┴ ┴┴
st ────────────────────────────────────────────────────────────────────────────────┘└┘└
744 { rw times_cont_diff_on_top at hf hg ⊢,
id └────────────────────┘
src └─┘└────────────────────┘└─────────┘
typ └─┘└────────────────────┘└─────────┘
doc └─┘ └─────────┘
txt └─┘ └─────────┘
par └─┘ └─────────┘
pid ┴ └─────────┘
st ───────────────────────────────────────┘└─
745 assume n,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ───────────┘└─
746 apply Itop n (hf n) (hg n) }
id └──┘ └┘ └┘ ┴
src └────┘ ┴ ┴ ┴ └┘ ┴ └┘
typ └────┘└──┘┴ ┴ └┘┴ └┘ └┘┴┴└┘
doc └────┘ ┴ ┴ ┴ └┘ ┴ └┘
txt └────┘ ┴ ┴ ┴ └┘ ┴ └┘
par └────┘ ┴ ┴ ┴ └┘ ┴ └┘
pid ┴ ┴ ┴ ┴ └┘ ┴ ┴┴
st ──────────────────────────────┘└─
747 end
st ──┘
748
749 /--
750 The cartesian product of `C^n` functions is `C^n`.
751 -/
752 lemma times_cont_diff.prod {n : with_top ℕ} {f : E → F} {g : E → G}
id └──────┘ ┴ ┴ ┴ ┴ ┴
src └──────┘ ┴
typ └──────┘ ┴ ┴ ┴ ┴ ┴
753 (hf : times_cont_diff 𝕜 n f) (hg : times_cont_diff 𝕜 n g) :
id └─────────────┘ ┴ ┴ ┴ └─────────────┘ ┴ ┴ ┴
src └─────────────┘ └─────────────┘
typ └─────────────┘ ┴ ┴ ┴ └─────────────┘ ┴ ┴ ┴
doc └─────────────┘ └─────────────┘
754 times_cont_diff 𝕜 n (λx:E, (f x, g x)) :=
id └─────────────┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
src └─────────────┘ ┴
typ └─────────────┘ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴
doc └─────────────┘
755 times_cont_diff_on_univ.1 $ times_cont_diff_on.prod (times_cont_diff_on_univ.2 hf)
id └─────────────────────┘┴ └─────────────────────┘ └─────────────────────┘┴ └┘
src └─────────────────────┘┴ └─────────────────────┘ └─────────────────────┘┴
typ └─────────────────────┘┴ └─────────────────────┘ └─────────────────────┘┴ └┘
doc └─────────────────────┘
756 (times_cont_diff_on_univ.2 hg) is_open_univ.unique_diff_on
id └─────────────────────┘┴ └┘ └──────────┘└─────────────┘
src └─────────────────────┘┴ └──────────┘└─────────────┘
typ └─────────────────────┘┴ └┘ └──────────┘└─────────────┘
757
758 /--
759 The composition of `C^n` functions on domains is `C^n`.
760 -/
761 lemma times_cont_diff_on.comp {n : with_top ℕ} {s : set E} {t : set F} {g : F → G} {f : E → F}
id └──────┘ ┴ └─┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴
src └──────┘ ┴ └─┘ └─┘
typ └──────┘ ┴ └─┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴
762 (hg : times_cont_diff_on 𝕜 n g t) (hf : times_cont_diff_on 𝕜 n f s) (hs : unique_diff_on 𝕜 s)
id └────────────────┘ ┴ ┴ ┴ ┴ └────────────────┘ ┴ ┴ ┴ ┴ └────────────┘ ┴ ┴
src └────────────────┘ └────────────────┘ └────────────┘
typ └────────────────┘ ┴ ┴ ┴ ┴ └────────────────┘ ┴ ┴ ┴ ┴ └────────────┘ ┴ ┴
doc └────────────────┘ └────────────────┘ └────────────┘
763 (st : s ⊆ f ⁻¹' t) : times_cont_diff_on 𝕜 n (g ∘ f) s :=
id ┴ ┴ ┴ └─┘ ┴ └────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └─┘ └────────────────┘ ┴
typ ┴ ┴ ┴ └─┘ ┴ └────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └─┘ └────────────────┘
764 begin
st └─────
765 tactic.unfreeze_local_instances,
id └─────────────────────────────┘
src └─────────────────────────────┘
typ └─────────────────────────────┘
doc └─────────────────────────────┘
par └─────────────────────────────┘
st ───────────────────────────────────
766 induction n using with_top.nat_induction with n IH Itop generalizing E F G,
id ┴
src └────────┘ └─────────────────────────────────────────────────────────────┘
typ └────────┘┴└─────────────────────────────────────────────────────────────┘
doc └────────┘ └─────────────────────────────────────────────────────────────┘
txt └────────┘ └─────────────────────────────────────────────────────────────┘
par └────────┘ └─────────────────────────────────────────────────────────────┘
pid ┴ └───────────────────────────┘└─────────────┘└─────────────────┘
st ───────────────────────────────────────────────────────────────────────────┘└─
767 { rw times_cont_diff_on_zero at hf hg ⊢,
id └─────────────────────┘
src └─┘└─────────────────────┘└─────────┘
typ └─┘└─────────────────────┘└─────────┘
doc └─┘ └─────────┘
txt └─┘ └─────────┘
par └─┘ └─────────┘
pid ┴ └─────────┘
st ───┘└───────────────────────────────────┘└─
768 exact continuous_on.comp hg hf st },
id └────────────────┘ └┘ └┘ └┘
src └────┘└────────────────┘┴ ┴ ┴ ┴
typ └────┘└────────────────┘┴└┘┴└┘┴└┘┴
doc └────┘ ┴ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴
st ─────────────────────────────────────┘└┘└
769 { rw times_cont_diff_on_succ at hf hg ⊢,
id └─────────────────────┘
src └─┘└─────────────────────┘└─────────┘
typ └─┘└─────────────────────┘└─────────┘
doc └─┘ └─────────┘
txt └─┘ └─────────┘
par └─┘ └─────────┘
pid ┴ └─────────┘
st ───┘└───────────────────────────────────┘└─
770 /- We have to show that the derivative of g ∘ f is C^n, given that g and f are C^(n+1).
st ────────────────────────────────────────────────────────────────────────────────────────────
771 By the chain rule, this derivative is Dg(f x) ⬝ Df(x). This is the composition of
st ──────────────────────────────────────────────────────────────────────────────────────
772 x ↦ (Dg (f x), Df (x)) with the product of bounded linear maps, which is bilinear and therefore
st ────────────────────────────────────────────────────────────────────────────────────────────────────
773 C^∞. By the induction assumption, it suffices to show that x ↦ (Dg (f x), Df (x)) is C^n. It
st ─────────────────────────────────────────────────────────────────────────────────────────────────
774 is even enough to show that each component is C^n. This follows from the assumptions on f and g,
st ─────────────────────────────────────────────────────────────────────────────────────────────────────
775 and the inductive assumption.
st ──────────────────────────────────
776 -/
st ───────
777 refine ⟨differentiable_on.comp hg.1 hf.1 st, _⟩,
id └────────────────────┘ └┘ └┘ └┘
src └─────┘ └────────────────────┘┴ └─┘ └─┘ └──┘
typ └─────┘ └────────────────────┘┴└┘└─┘└┘└─┘└┘└──┘
doc └─────┘ ┴ └─┘ └─┘ └──┘
txt └─────┘ ┴ └─┘ └─┘ └──┘
par └─────┘ ┴ └─┘ └─┘ └──┘
pid ┴ ┴ └─┘ └─┘ └──┘
st ──────────────────────────────────────────────────┘└─
778 have : ∀x∈s, fderiv_within 𝕜 (g ∘ f) s x =
id ┴ ┴
src └─────┘ └┘ ┴ ┴ ┴ ┴┴┴ └┘ ┴ ┴┴└
typ └─────┘ └┘ ┴ ┴ ┴ ┴┴┴ └┘ ┴ ┴┴└
doc └─────┘ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └
txt └─────┘ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └
par └─────┘ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └
pid └───┘└┘ └┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ └
st ───────────────────────────────────────────────
779 continuous_linear_map.comp (fderiv_within 𝕜 g t (f x)) (fderiv_within 𝕜 f s x),
id └────────────────────────┘ ┴ ┴ └───────────┘ ┴ ┴ ┴
src ─────┘└────────────────────────┘┴ ┴ ┴ ┴ ┴ ┴ └─┘ └───────────┘┴ ┴ ┴ ┴ ┴
typ ─────┘└────────────────────────┘┴ ┴ ┴┴┴┴┴ ┴ └─┘ └───────────┘┴┴┴┴┴┴┴ ┴
doc ─────┘└────────────────────────┘┴ ┴ ┴ ┴ ┴ ┴ └─┘ └───────────┘┴ ┴ ┴ ┴ ┴
txt ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴
par ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴
pid ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴
st ───────────────────────────────────────────────────────────────────────────────────┘└─
780 { assume x hx,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────────┘
st ─────┘└─────────┘└─
781 apply fderiv_within.comp x _ (hf.1 x hx) st (hs x hx),
id └────────────────┘ └┘ └┘ └┘ ┴ └┘
src └────┘└────────────────┘┴ └─┘ └─┘ ┴ └┘ ┴ ┴ ┴ ┴
typ └────┘└────────────────┘┴ └─┘ └┘└─┘ ┴ └┘└┘┴ └┘┴┴┴└┘┴
doc └────┘ ┴ └─┘ └─┘ ┴ └┘ ┴ ┴ ┴ ┴
txt └────┘ ┴ └─┘ └─┘ ┴ └┘ ┴ ┴ ┴ ┴
par └────┘ ┴ └─┘ └─┘ ┴ └┘ ┴ ┴ ┴ ┴
pid ┴ ┴ └─┘ └─┘ ┴ └┘ ┴ ┴ ┴ ┴
st ──────────────────────────────────────────────────────────┘└─
782 exact hg.1 _ (st hx) },
id └┘ └┘ └┘
src └────┘ └───┘ ┴ └┘
typ └────┘└┘└───┘ └┘┴└┘└┘
doc └────┘ └───┘ ┴ └┘
txt └────┘ └───┘ ┴ └┘
par └────┘ └───┘ ┴ └┘
pid ┴ └───┘ ┴ ┴┴
st ──────────────────────────┘└┘└
783 apply times_cont_diff_on.congr _ hs this,
id └──────────────────────┘ └┘ └──┘
src └────┘└──────────────────────┘└─┘ ┴
typ └────┘└──────────────────────┘└─┘└┘┴└──┘
doc └────┘ └─┘ ┴
txt └────┘ └─┘ ┴
par └────┘ └─┘ ┴
pid ┴ └─┘ ┴
st ───────────────────────────────────────────┘└─
784 have A : times_cont_diff_on 𝕜 n (λx, fderiv_within 𝕜 g t (f x)) s :=
id └────────────────┘ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴
src └───────┘└────────────────┘┴ ┴ ┴ └─┘└───────────┘┴ ┴ ┴ ┴ ┴ └─┘ └───
typ └───────┘└────────────────┘┴ ┴┴┴ └─┘└───────────┘┴┴┴┴┴┴┴ ┴┴ └─┘┴└───
doc └───────┘└────────────────┘┴ ┴ ┴ └─┘└───────────┘┴ ┴ ┴ ┴ ┴ └─┘ └───
txt └───────┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └─┘ └───
par └───────┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └─┘ └───
pid └────┘└─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └─┘ └───
st ─────────────────────────────────────────────────────────────────────────
785 IH hg.2 (times_cont_diff_on_succ.2 hf).of_succ hs st,
id └┘ └┘ └─────────────────────┘ └┘ └┘ └┘
src ─────┘ ┴ └─┘ └─────────────────────┘└─┘ └────────┘ ┴
typ ─────┘└┘┴└┘└─┘ └─────────────────────┘└─┘└┘└────────┘└┘┴└┘
doc ─────┘ ┴ └─┘ └─┘ └────────┘ ┴
txt ─────┘ ┴ └─┘ └─┘ └────────┘ ┴
par ─────┘ ┴ └─┘ └─┘ └────────┘ ┴
pid ─────┘ ┴ └─┘ └─┘ └────────┘ ┴
st ─────────────────────────────────────────────────────────┘└─
786 have B : times_cont_diff_on 𝕜 n (λx, fderiv_within 𝕜 f s x) s := hf.2,
id └────────────────┘ ┴ └───────────┘ ┴ ┴ ┴ └┘
src └───────┘└────────────────┘┴ ┴ ┴ └─┘└───────────┘┴ ┴ ┴ ┴ └┘ └──┘ └┘
typ └───────┘└────────────────┘┴ ┴┴┴ └─┘└───────────┘┴┴┴┴┴ ┴ └┘┴└──┘└┘└┘
doc └───────┘└────────────────┘┴ ┴ ┴ └─┘└───────────┘┴ ┴ ┴ ┴ └┘ └──┘ └┘
txt └───────┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └┘ └──┘ └┘
par └───────┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └┘ └──┘ └┘
pid └────┘└─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └┘ └──┘ └┘
st ────────────────────────────────────────────────────────────────────────┘└─
787 have C : times_cont_diff_on 𝕜 n (λx:E, (fderiv_within 𝕜 f s x, fderiv_within 𝕜 g t (f x))) s :=
id └────────────────┘ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴ ┴
src └───────┘└────────────────┘┴ ┴ ┴ └┘ └┘┴ ┴ ┴ ┴ ┴ └┘└───────────┘┴ ┴ ┴ ┴ ┴ └──┘ └───
typ └───────┘└────────────────┘┴ ┴┴┴ └┘┴└┘┴ ┴ ┴ ┴ ┴ └┘└───────────┘┴┴┴┴┴┴┴ ┴┴ └──┘┴└───
doc └───────┘└────────────────┘┴ ┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴ └┘└───────────┘┴ ┴ ┴ ┴ ┴ └──┘ └───
txt └───────┘ ┴ ┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └──┘ └───
par └───────┘ ┴ ┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └──┘ └───
pid └────┘└─┘ ┴ ┴ ┴ └┘ └┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ └──┘ └───
st ────────────────────────────────────────────────────────────────────────────────────────────────────
788 times_cont_diff_on.prod B A hs,
id └─────────────────────┘ ┴ ┴ └┘
src ─────┘└─────────────────────┘┴ ┴ ┴
typ ─────┘└─────────────────────┘┴┴┴┴┴└┘
doc ─────┘└─────────────────────┘┴ ┴ ┴
txt ─────┘ ┴ ┴ ┴
par ─────┘ ┴ ┴ ┴
pid ─────┘ ┴ ┴ ┴
st ───────────────────────────────────┘└─
789 have D : times_cont_diff_on 𝕜 n (λ(p : (E →L[𝕜] F) × (F →L[𝕜] G)), p.2.comp p.1) univ :=
id └────────────────┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ └──┘
src └───────┘└────────────────┘┴ ┴ ┴ └───┘ ┴└─┘ ┴┴ └┘┴┴ ┴ ┴ └──┘ └──────┘ └──┘└──┘└───
typ └───────┘└────────────────┘┴ ┴┴┴ └───┘ ┴┴└─┘ ┴┴ └┘┴┴ ┴┴ ┴ ┴┴└──┘ └──────┘ └──┘└──┘└───
doc └───────┘└────────────────┘┴ ┴ ┴ └───┘ ┴└─┘ ┴┴ └┘ ┴ ┴ ┴ └──┘ └──────┘ └──┘ └───
txt └───────┘ ┴ ┴ ┴ └───┘ ┴ ┴ └┘ ┴ ┴ ┴ └──┘ └──────┘ └──┘ └───
par └───────┘ ┴ ┴ ┴ └───┘ ┴ ┴ └┘ ┴ ┴ ┴ └──┘ └──────┘ └──┘ └───
pid └────┘└─┘ ┴ ┴ ┴ └───┘ ┴ ┴ └┘ ┴ ┴ ┴ └──┘ └──────┘ └──┘ └───
st ─────────────────────────────────────────────────────────────────────────────────────────────
790 is_bounded_bilinear_map_comp.times_cont_diff.times_cont_diff_on is_open_univ.unique_diff_on,
id └─────────────────────────────────────────────────────────────┘ └─────────────────────────┘
src ─────┘└─────────────────────────────────────────────────────────────┘┴└─────────────────────────┘
typ ─────┘└─────────────────────────────────────────────────────────────┘┴└─────────────────────────┘
doc ─────┘ ┴
txt ─────┘ ┴
par ─────┘ ┴
pid ─────┘ ┴
st ────────────────────────────────────────────────────────────────────────────────────────────────┘└─
791 exact IH D C hs (subset_univ _) },
id └┘ ┴ ┴ └┘ └─────────┘
src └────┘ ┴ ┴ ┴ ┴ └─────────┘└──┘
typ └────┘└┘┴┴┴┴┴└┘┴ └─────────┘└──┘
doc └────┘ ┴ ┴ ┴ ┴ └──┘
txt └────┘ ┴ ┴ ┴ ┴ └──┘
par └────┘ ┴ ┴ ┴ ┴ └──┘
pid ┴ ┴ ┴ ┴ ┴ └─┘┴
st ───────────────────────────────────┘└┘└
792 { rw times_cont_diff_on_top at hf hg ⊢,
id └────────────────────┘
src └─┘└────────────────────┘└─────────┘
typ └─┘└────────────────────┘└─────────┘
doc └─┘ └─────────┘
txt └─┘ └─────────┘
par └─┘ └─────────┘
pid ┴ └─────────┘
st ───────────────────────────────────────┘└─
793 assume n,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ───────────┘└─
794 apply Itop n (hg n) (hf n) hs st }
id └──┘ └┘ └┘ ┴ └┘ └┘
src └────┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴
typ └────┘└──┘┴ ┴ └┘┴ └┘ └┘┴┴└┘└┘┴└┘┴
doc └────┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴
txt └────┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴
par └────┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴
pid ┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴
st ────────────────────────────────────┘└─
795 end
st ──┘
796
797 /--
798 The composition of a C^n function on domain with a C^n function is C^n.
799 -/
800 lemma times_cont_diff.comp_times_cont_diff_on {n : with_top ℕ} {s : set E} {g : F → G} {f : E → F}
id └──────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴
src └──────┘ ┴ └─┘
typ └──────┘ ┴ └─┘ ┴ ┴ ┴ ┴ ┴
801 (hg : times_cont_diff 𝕜 n g) (hf : times_cont_diff_on 𝕜 n f s) (hs : unique_diff_on 𝕜 s) :
id └─────────────┘ ┴ ┴ ┴ └────────────────┘ ┴ ┴ ┴ ┴ └────────────┘ ┴ ┴
src └─────────────┘ └────────────────┘ └────────────┘
typ └─────────────┘ ┴ ┴ ┴ └────────────────┘ ┴ ┴ ┴ ┴ └────────────┘ ┴ ┴
doc └─────────────┘ └────────────────┘ └────────────┘
802 times_cont_diff_on 𝕜 n (g ∘ f) s :=
id └────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └────────────────┘ ┴
typ └────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └────────────────┘
803 (times_cont_diff_on_univ.2 hg).comp hf hs subset_preimage_univ
id └─────────────────────┘┴ └┘ └──┘ └┘ └┘ └──────────────────┘
src └─────────────────────┘┴ └──┘ └──────────────────┘
typ └─────────────────────┘┴ └┘ └──┘ └┘ └┘ └──────────────────┘
doc └──┘
804
805 /--
806 The composition of `C^n` functions is `C^n`.
807 -/
808 lemma times_cont_diff.comp {n : with_top ℕ} {g : F → G} {f : E → F}
id └──────┘ ┴ ┴ ┴ ┴ ┴
src └──────┘ ┴
typ └──────┘ ┴ ┴ ┴ ┴ ┴
809 (hg : times_cont_diff 𝕜 n g) (hf : times_cont_diff 𝕜 n f) :
id └─────────────┘ ┴ ┴ ┴ └─────────────┘ ┴ ┴ ┴
src └─────────────┘ └─────────────┘
typ └─────────────┘ ┴ ┴ ┴ └─────────────┘ ┴ ┴ ┴
doc └─────────────┘ └─────────────┘
810 times_cont_diff 𝕜 n (g ∘ f) :=
id └─────────────┘ ┴ ┴ ┴ ┴ ┴
src └─────────────┘ ┴
typ └─────────────┘ ┴ ┴ ┴ ┴ ┴
doc └─────────────┘
811 times_cont_diff_on_univ.1 $ times_cont_diff_on.comp (times_cont_diff_on_univ.2 hg)
id └─────────────────────┘┴ └─────────────────────┘ └─────────────────────┘┴ └┘
src └─────────────────────┘┴ └─────────────────────┘ └─────────────────────┘┴
typ └─────────────────────┘┴ └─────────────────────┘ └─────────────────────┘┴ └┘
doc └─────────────────────┘
812 (times_cont_diff_on_univ.2 hf) is_open_univ.unique_diff_on (subset_univ _)
id └─────────────────────┘┴ └┘ └──────────┘└─────────────┘ └─────────┘
src └─────────────────────┘┴ └──────────┘└─────────────┘ └─────────┘
typ └─────────────────────┘┴ └┘ └──────────┘└─────────────┘ └─────────┘
813
814 /--
815 The bundled derivative of a `C^{n+1}` function is `C^n`.
816 -/
817 lemma times_cont_diff_on_fderiv_within_apply {m n : with_top ℕ} {s : set E}
id └──────┘ ┴ └─┘ ┴
src └──────┘ ┴ └─┘
typ └──────┘ ┴ └─┘ ┴
818 {f : E → F} (hf : times_cont_diff_on 𝕜 n f s) (hs : unique_diff_on 𝕜 s) (hmn : m + 1 ≤ n) :
id ┴ ┴ └────────────────┘ ┴ ┴ ┴ ┴ └────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └────────────────┘ └────────────┘ ┴ ┴
typ ┴ ┴ └────────────────┘ ┴ ┴ ┴ ┴ └────────────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └────────────────┘ └────────────┘
819 times_cont_diff_on 𝕜 m (λp : E × E, (fderiv_within 𝕜 f s p.1 : E →L[𝕜] F) p.2) (set.prod s (univ : set E)) :=
id └────────────────┘ ┴ ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴┴ ┴ └─┘┴┴ ┴ ┴┴ └──────┘ ┴ └──┘ └─┘ ┴
src └────────────────┘ ┴ └───────────┘ ┴ └─┘ ┴ ┴ └──────┘ └──┘ └─┘
typ └────────────────┘ ┴ ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴ ┴┴ ┴ └─┘┴┴ ┴ ┴┴ └──────┘ ┴ └──┘ └─┘ ┴
doc └────────────────┘ └───────────┘ └─┘ ┴ └──────┘
820 begin
st └─────
821 have U : unique_diff_on 𝕜 (set.prod s (univ : set E)) :=
id └────────────┘ ┴ └──────┘ ┴ └──┘ └─┘ ┴
src └───────┘└────────────┘┴ ┴ └──────┘┴ ┴ └──┘└─┘└─┘┴ └─────
typ └───────┘└────────────┘┴┴┴ └──────┘┴┴┴ └──┘└─┘└─┘┴┴└─────
doc └───────┘└────────────┘┴ ┴ └──────┘┴ ┴ └─┘ ┴ └─────
txt └───────┘ ┴ ┴ ┴ ┴ └─┘ ┴ └─────
par └───────┘ ┴ ┴ ┴ ┴ └─┘ ┴ └─────
pid └────┘└─┘ ┴ ┴ ┴ ┴ └─┘ ┴ └┘└───
st ───────────────────────────────────────────────────────────
822 hs.prod unique_diff_on_univ,
id └─────┘ └─────────────────┘
src ───┘└─────┘┴└─────────────────┘
typ ───┘└─────┘┴└─────────────────┘
doc ───┘└─────┘┴
txt ───┘ ┴
par ───┘ ┴
pid ───┘ ┴
st ──────────────────────────────┘└─
823 have A : times_cont_diff 𝕜 m (λp : (E →L[𝕜] F) × E, p.1 p.2),
id └─────────────┘ ┴ └─┘┴┴ ┴ ┴ ┴
src └───────┘└─────────────┘┴ ┴ ┴ └──┘ ┴└─┘ ┴┴ └┘┴┴ └┘ └─┘ └─┘
typ └───────┘└─────────────┘┴ ┴┴┴ └──┘ ┴└─┘┴┴┴┴└┘┴┴┴└┘ └─┘ └─┘
doc └───────┘└─────────────┘┴ ┴ ┴ └──┘ ┴└─┘ ┴┴ └┘ ┴ └┘ └─┘ └─┘
txt └───────┘ ┴ ┴ ┴ └──┘ ┴ ┴ └┘ ┴ └┘ └─┘ └─┘
par └───────┘ ┴ ┴ ┴ └──┘ ┴ ┴ └┘ ┴ └┘ └─┘ └─┘
pid └────┘└─┘ ┴ ┴ ┴ └──┘ ┴ ┴ └┘ ┴ └┘ └─┘ └─┘
st ─────────────────────────────────────────────────────────────┘└─
824 { apply is_bounded_bilinear_map.times_cont_diff,
id └─────────────────────────────────────┘
src └────┘└─────────────────────────────────────┘
typ └────┘└─────────────────────────────────────┘
doc └────┘└─────────────────────────────────────┘
txt └────┘
par └────┘
pid ┴
st ───┘└───────────────────────────────────────────┘└─
825 exact is_bounded_bilinear_map_apply },
id └───────────────────────────┘
src └────┘└───────────────────────────┘┴
typ └────┘└───────────────────────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───────────────────────────────────────┘└┘└
826 have B : times_cont_diff_on 𝕜 m
id └────────────────┘ ┴
src └───────┘└────────────────┘┴ ┴ └
typ └───────┘└────────────────┘┴ ┴┴└
doc └───────┘└────────────────┘┴ ┴ └
txt └───────┘ ┴ ┴ └
par └───────┘ ┴ ┴ └
pid └────┘└─┘ ┴ ┴ └
st ──────────────────────────────────
827 (λ (p : E × E), ((fderiv_within 𝕜 f s p.fst), p.snd)) (set.prod s univ),
id ┴ ┴ ┴ └───────────┘ ┴ ┴ └──┘ └──┘ └──────┘ ┴ └──┘
src ───┘ └────┘ ┴ ┴ └─┘┴ └───────────┘┴ ┴ ┴ ┴ └──┘└─┘ └──┘└─┘ └──────┘┴ ┴└──┘┴
typ ───┘ └────┘ ┴┴┴┴└─┘┴ └───────────┘┴┴┴┴┴ ┴ └──┘└─┘ └──┘└─┘ └──────┘┴┴┴└──┘┴
doc ───┘ └────┘ ┴ ┴ └─┘ └───────────┘┴ ┴ ┴ ┴ └─┘ └─┘ └──────┘┴ ┴ ┴
txt ───┘ └────┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └─┘ └─┘ ┴ ┴ ┴
par ───┘ └────┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └─┘ └─┘ ┴ ┴ ┴
pid ───┘ └────┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └─┘ └─┘ ┴ ┴ ┴
st ──────────────────────────────────────────────────────────────────────────┘└─
828 { apply times_cont_diff_on.prod _ _ U,
id └─────────────────────┘ ┴
src └────┘└─────────────────────┘└───┘
typ └────┘└─────────────────────┘└───┘┴
doc └────┘└─────────────────────┘└───┘
txt └────┘ └───┘
par └────┘ └───┘
pid ┴ └───┘
st ───┘└─────────────────────────────────┘└─
829 { have I : times_cont_diff_on 𝕜 m (λ (x : E), fderiv_within 𝕜 f s x) s :=
id └────────────────┘ ┴ ┴ └───────────┘ ┴ ┴ ┴
src └───────┘└────────────────┘┴ ┴ ┴ └────┘ └─┘└───────────┘┴ ┴ ┴ ┴ └┘ └───
typ └───────┘└────────────────┘┴ ┴┴┴ └────┘┴└─┘└───────────┘┴┴┴┴┴ ┴ └┘┴└───
doc └───────┘└────────────────┘┴ ┴ ┴ └────┘ └─┘└───────────┘┴ ┴ ┴ ┴ └┘ └───
txt └───────┘ ┴ ┴ ┴ └────┘ └─┘ ┴ ┴ ┴ ┴ └┘ └───
par └───────┘ ┴ ┴ ┴ └────┘ └─┘ ┴ ┴ ┴ ┴ └┘ └───
pid └────┘└─┘ ┴ ┴ ┴ └────┘ └─┘ ┴ ┴ ┴ ┴ └┘ └───
st ─────┘└───────────────────────────────────────────────────────────────────────
830 times_cont_diff_on_fderiv_within hf hmn,
id └──────────────────────────────┘ └┘ └─┘
src ───────┘└──────────────────────────────┘┴ ┴
typ ───────┘└──────────────────────────────┘┴└┘┴└─┘
doc ───────┘ ┴ ┴
txt ───────┘ ┴ ┴
par ───────┘ ┴ ┴
pid ───────┘ ┴ ┴
st ──────────────────────────────────────────────┘└─
831 have J : times_cont_diff_on 𝕜 m (λ (x : E × E), x.1) (set.prod s univ) :=
id └────────────────┘ ┴ ┴ ┴ └──────┘ ┴ └──┘
src └───────┘└────────────────┘┴ ┴ ┴ └────┘ ┴ ┴ └─┘ └──┘ └──────┘┴ ┴└──┘└────
typ └───────┘└────────────────┘┴┴┴┴┴ └────┘ ┴ ┴┴└─┘ └──┘ └──────┘┴┴┴└──┘└────
doc └───────┘└────────────────┘┴ ┴ ┴ └────┘ ┴ ┴ └─┘ └──┘ └──────┘┴ ┴ └────
txt └───────┘ ┴ ┴ ┴ └────┘ ┴ ┴ └─┘ └──┘ ┴ ┴ └────
par └───────┘ ┴ ┴ ┴ └────┘ ┴ ┴ └─┘ └──┘ ┴ ┴ └────
pid └────┘└─┘ ┴ ┴ ┴ └────┘ ┴ ┴ └─┘ └──┘ ┴ ┴ ┴└───
st ────────────────────────────────────────────────────────────────────────────────
832 times_cont_diff_fst.times_cont_diff_on U,
id └────────────────────────────────────┘ ┴
src ───────┘└────────────────────────────────────┘┴
typ ───────┘└────────────────────────────────────┘┴┴
doc ───────┘└────────────────────────────────────┘┴
txt ───────┘ ┴
par ───────┘ ┴
pid ───────┘ ┴
st ───────────────────────────────────────────────┘└─
833 exact times_cont_diff_on.comp I J U (prod_subset_preimage_fst _ _) },
id └─────────────────────┘ ┴ ┴ ┴ └──────────────────────┘
src └────┘└─────────────────────┘┴ ┴ ┴ ┴ └──────────────────────┘└────┘
typ └────┘└─────────────────────┘┴┴┴┴┴┴┴ └──────────────────────┘└────┘
doc └────┘└─────────────────────┘┴ ┴ ┴ ┴ └────┘
txt └────┘ ┴ ┴ ┴ ┴ └────┘
par └────┘ ┴ ┴ ┴ ┴ └────┘
pid ┴ ┴ ┴ ┴ ┴ └───┘┴
st ────────────────────────────────────────────────────────────────────────┘└┘└
834 { apply times_cont_diff.times_cont_diff_on _ U,
id └────────────────────────────────┘ ┴
src └────┘└────────────────────────────────┘└─┘
typ └────┘└────────────────────────────────┘└─┘┴
doc └────┘ └─┘
txt └────┘ └─┘
par └────┘ └─┘
pid ┴ └─┘
st ─────────────────────────────────────────────────┘└─
835 apply is_bounded_linear_map.times_cont_diff,
id └───────────────────────────────────┘
src └────┘└───────────────────────────────────┘
typ └────┘└───────────────────────────────────┘
doc └────┘└───────────────────────────────────┘
txt └────┘
par └────┘
pid ┴
st ────────────────────────────────────────────────┘└─
836 apply is_bounded_linear_map.snd } },
id └───────────────────────┘
src └────┘└───────────────────────┘┴
typ └────┘└───────────────────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ─────────────────────────────────────┘└──┘└
837 exact A.comp_times_cont_diff_on B U
id └───────────────────────┘ ┴ ┴
src └────┘└───────────────────────┘┴ ┴ ┴
typ └────┘└───────────────────────┘┴┴┴┴┴
doc └────┘└───────────────────────┘┴ ┴ ┴
txt └────┘ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ─────────────────────────────────────┘
838 end
st └─┘
839
840 /--
841 The bundled derivative of a `C^{n+1}` function is `C^n`.
842 -/
843 lemma times_cont_diff.times_cont_diff_fderiv_apply {n m : with_top ℕ} {s : set E} {f : E → F}
id └──────┘ ┴ └─┘ ┴ ┴ ┴
src └──────┘ ┴ └─┘
typ └──────┘ ┴ └─┘ ┴ ┴ ┴
844 (hf : times_cont_diff 𝕜 n f) (hmn : m + 1 ≤ n) :
id └─────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─────────────┘ ┴ ┴
typ └─────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────────────┘
845 times_cont_diff 𝕜 m (λp : E × E, (fderiv 𝕜 f p.1 : E →L[𝕜] F) p.2) :=
id └─────────────┘ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴┴ ┴ └─┘┴┴ ┴ ┴┴
src └─────────────┘ ┴ └────┘ ┴ └─┘ ┴ ┴
typ └─────────────┘ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴┴ ┴ └─┘┴┴ ┴ ┴┴
doc └─────────────┘ └────┘ └─┘ ┴
846 begin
st └─────
847 rw ← times_cont_diff_on_univ at ⊢ hf,
id └─────────────────────┘
src └───┘└─────────────────────┘└──────┘
typ └───┘└─────────────────────┘└──────┘
doc └───┘ └──────┘
txt └───┘ └──────┘
par └───┘ └──────┘
pid └─┘ └──────┘
st ─────────────────────────────────────┘└─
848 rw [← fderiv_within_univ, ← univ_prod_univ],
id └────────────────┘ └────────────┘
src └────┘└────────────────┘└──┘└────────────┘┴
typ └────┘└────────────────┘└──┘└────────────┘┴
doc └────┘ └──┘ ┴
txt └────┘ └──┘ ┴
par └────┘ └──┘ ┴
pid └──┘ └──┘ ┴
st ─────────────────────────┘└────────────────┘└──
849 exact times_cont_diff_on_fderiv_within_apply hf unique_diff_on_univ hmn
id └────────────────────────────────────┘ └┘ └─────────────────┘ └─┘
src └────┘└────────────────────────────────────┘┴ ┴└─────────────────┘┴ ┴
typ └────┘└────────────────────────────────────┘┴└┘┴└─────────────────┘┴└─┘┴
doc └────┘└────────────────────────────────────┘┴ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴
st ─────────────────────────────────────────────────────────────────────────┘
850 end
st └─┘
851
852 /--
853 The sum of two C^n functions on a domain is C^n.
854 -/
855 lemma times_cont_diff_on.add {n : with_top ℕ} {s : set E} {f g : E → F}
id └──────┘ ┴ └─┘ ┴ ┴ ┴
src └──────┘ ┴ └─┘
typ └──────┘ ┴ └─┘ ┴ ┴ ┴
856 (hf : times_cont_diff_on 𝕜 n f s) (hg : times_cont_diff_on 𝕜 n g s) (hs : unique_diff_on 𝕜 s) :
id └────────────────┘ ┴ ┴ ┴ ┴ └────────────────┘ ┴ ┴ ┴ ┴ └────────────┘ ┴ ┴
src └────────────────┘ └────────────────┘ └────────────┘
typ └────────────────┘ ┴ ┴ ┴ ┴ └────────────────┘ ┴ ┴ ┴ ┴ └────────────┘ ┴ ┴
doc └────────────────┘ └────────────────┘ └────────────┘
857 times_cont_diff_on 𝕜 n (λx, f x + g x) s :=
id └────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └────────────────┘ ┴
typ └────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └────────────────┘
858 begin
st └─────
859 have : times_cont_diff 𝕜 n (λp : F × F, p.1 + p.2),
id └─────────────┘ ┴ ┴ ┴ ┴ ┴
src └─────┘└─────────────┘┴ ┴ ┴ └──┘ ┴┴┴ └┘ └─┘┴┴ └─┘
typ └─────┘└─────────────┘┴┴┴┴┴ └──┘ ┴┴┴┴└┘ └─┘┴┴ └─┘
doc └─────┘└─────────────┘┴ ┴ ┴ └──┘ ┴ ┴ └┘ └─┘ ┴ └─┘
txt └─────┘ ┴ ┴ ┴ └──┘ ┴ ┴ └┘ └─┘ ┴ └─┘
par └─────┘ ┴ ┴ ┴ └──┘ ┴ ┴ └┘ └─┘ ┴ └─┘
pid └───┘└┘ ┴ ┴ ┴ └──┘ ┴ ┴ └┘ └─┘ ┴ └─┘
st ───────────────────────────────────────────────────┘└─
860 { apply is_bounded_linear_map.times_cont_diff,
id └───────────────────────────────────┘
src └────┘└───────────────────────────────────┘
typ └────┘└───────────────────────────────────┘
doc └────┘└───────────────────────────────────┘
txt └────┘
par └────┘
pid ┴
st ───┘└─────────────────────────────────────────┘└─
861 exact is_bounded_linear_map.add is_bounded_linear_map.fst is_bounded_linear_map.snd },
id └───────────────────────┘ └───────────────────────┘ └───────────────────────┘
src └────┘└───────────────────────┘┴└───────────────────────┘┴└───────────────────────┘┴
typ └────┘└───────────────────────┘┴└───────────────────────┘┴└───────────────────────┘┴
doc └────┘ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ───────────────────────────────────────────────────────────────────────────────────────┘└┘└
862 exact this.comp_times_cont_diff_on (hf.prod hg hs) hs
id └──────────────────────────┘ └─────┘ └┘ └┘
src └────┘└──────────────────────────┘┴ └─────┘┴ ┴ └┘ ┴
typ └────┘└──────────────────────────┘┴ └─────┘┴└┘┴ └┘└┘┴
doc └────┘└──────────────────────────┘┴ └─────┘┴ ┴ └┘ ┴
txt └────┘ ┴ ┴ ┴ └┘ ┴
par └────┘ ┴ ┴ ┴ └┘ ┴
pid ┴ ┴ ┴ ┴ └┘ ┴
st ───────────────────────────────────────────────────────┘
863 end
st └─┘
864
865 /--
866 The sum of two C^n functions is C^n.
867 -/
868 lemma times_cont_diff.add {n : with_top ℕ} {f g : E → F}
id └──────┘ ┴ ┴ ┴
src └──────┘ ┴
typ └──────┘ ┴ ┴ ┴
869 (hf : times_cont_diff 𝕜 n f) (hg : times_cont_diff 𝕜 n g) : times_cont_diff 𝕜 n (λx, f x + g x) :=
id └─────────────┘ ┴ ┴ ┴ └─────────────┘ ┴ ┴ ┴ └─────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─────────────┘ └─────────────┘ └─────────────┘ ┴
typ └─────────────┘ ┴ ┴ ┴ └─────────────┘ ┴ ┴ ┴ └─────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────────────┘ └─────────────┘ └─────────────┘
870 begin
st └─────
871 have : times_cont_diff 𝕜 n (λp : F × F, p.1 + p.2),
id └─────────────┘ ┴ ┴ ┴ ┴ ┴
src └─────┘└─────────────┘┴ ┴ ┴ └──┘ ┴┴┴ └┘ └─┘┴┴ └─┘
typ └─────┘└─────────────┘┴┴┴┴┴ └──┘ ┴┴┴┴└┘ └─┘┴┴ └─┘
doc └─────┘└─────────────┘┴ ┴ ┴ └──┘ ┴ ┴ └┘ └─┘ ┴ └─┘
txt └─────┘ ┴ ┴ ┴ └──┘ ┴ ┴ └┘ └─┘ ┴ └─┘
par └─────┘ ┴ ┴ ┴ └──┘ ┴ ┴ └┘ └─┘ ┴ └─┘
pid └───┘└┘ ┴ ┴ ┴ └──┘ ┴ ┴ └┘ └─┘ ┴ └─┘
st ───────────────────────────────────────────────────┘└─
872 { apply is_bounded_linear_map.times_cont_diff,
id └───────────────────────────────────┘
src └────┘└───────────────────────────────────┘
typ └────┘└───────────────────────────────────┘
doc └────┘└───────────────────────────────────┘
txt └────┘
par └────┘
pid ┴
st ───┘└─────────────────────────────────────────┘└─
873 exact is_bounded_linear_map.add is_bounded_linear_map.fst is_bounded_linear_map.snd },
id └───────────────────────┘ └───────────────────────┘ └───────────────────────┘
src └────┘└───────────────────────┘┴└───────────────────────┘┴└───────────────────────┘┴
typ └────┘└───────────────────────┘┴└───────────────────────┘┴└───────────────────────┘┴
doc └────┘ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ───────────────────────────────────────────────────────────────────────────────────────┘└┘└
874 exact this.comp (hf.prod hg)
id └───────┘ └─────┘ └┘
src └────┘└───────┘┴ └─────┘┴ └┘
typ └────┘└───────┘┴ └─────┘┴└┘└┘
doc └────┘└───────┘┴ └─────┘┴ └┘
txt └────┘ ┴ ┴ └┘
par └────┘ ┴ ┴ └┘
pid ┴ ┴ ┴ ┴┴
st ──────────────────────────────┘
875 end
st └─┘
876
877 /--
878 The negative of a C^n function on a domain is C^n.
879 -/
880 lemma times_cont_diff_on.neg {n : with_top ℕ} {s : set E} {f : E → F}
id └──────┘ ┴ └─┘ ┴ ┴ ┴
src └──────┘ ┴ └─┘
typ └──────┘ ┴ └─┘ ┴ ┴ ┴
881 (hf : times_cont_diff_on 𝕜 n f s) (hs : unique_diff_on 𝕜 s) :
id └────────────────┘ ┴ ┴ ┴ ┴ └────────────┘ ┴ ┴
src └────────────────┘ └────────────┘
typ └────────────────┘ ┴ ┴ ┴ ┴ └────────────┘ ┴ ┴
doc └────────────────┘ └────────────┘
882 times_cont_diff_on 𝕜 n (λx, -f x) s :=
id └────────────────┘ ┴ ┴ ┴ ┴┴ ┴ ┴
src └────────────────┘ ┴
typ └────────────────┘ ┴ ┴ ┴ ┴┴ ┴ ┴
doc └────────────────┘
883 begin
st └─────
884 have : times_cont_diff 𝕜 n (λp : F, -p),
id └─────────────┘ ┴ ┴ ┴ ┴
src └─────┘└─────────────┘┴ ┴ ┴ └──┘ └┘┴ ┴
typ └─────┘└─────────────┘┴┴┴┴┴ └──┘┴└┘┴ ┴
doc └─────┘└─────────────┘┴ ┴ ┴ └──┘ └┘ ┴
txt └─────┘ ┴ ┴ ┴ └──┘ └┘ ┴
par └─────┘ ┴ ┴ ┴ └──┘ └┘ ┴
pid └───┘└┘ ┴ ┴ ┴ └──┘ └┘ ┴
st ────────────────────────────────────────┘└─
885 { apply is_bounded_linear_map.times_cont_diff,
id └───────────────────────────────────┘
src └────┘└───────────────────────────────────┘
typ └────┘└───────────────────────────────────┘
doc └────┘└───────────────────────────────────┘
txt └────┘
par └────┘
pid ┴
st ───┘└─────────────────────────────────────────┘└─
886 exact is_bounded_linear_map.neg is_bounded_linear_map.id },
id └───────────────────────┘ └──────────────────────┘
src └────┘└───────────────────────┘┴└──────────────────────┘┴
typ └────┘└───────────────────────┘┴└──────────────────────┘┴
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ────────────────────────────────────────────────────────────┘└┘└
887 exact this.comp_times_cont_diff_on hf hs
id └──────────────────────────┘ └┘ └┘
src └────┘└──────────────────────────┘┴ ┴ ┴
typ └────┘└──────────────────────────┘┴└┘┴└┘┴
doc └────┘└──────────────────────────┘┴ ┴ ┴
txt └────┘ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ──────────────────────────────────────────┘
888 end
st └─┘
889
890 /--
891 The negative of a C^n function is C^n.
892 -/
893 lemma times_cont_diff.neg {n : with_top ℕ} {f : E → F} (hf : times_cont_diff 𝕜 n f) :
id └──────┘ ┴ ┴ ┴ └─────────────┘ ┴ ┴ ┴
src └──────┘ ┴ └─────────────┘
typ └──────┘ ┴ ┴ ┴ └─────────────┘ ┴ ┴ ┴
doc └─────────────┘
894 times_cont_diff 𝕜 n (λx, -f x) :=
id └─────────────┘ ┴ ┴ ┴ ┴┴ ┴
src └─────────────┘ ┴
typ └─────────────┘ ┴ ┴ ┴ ┴┴ ┴
doc └─────────────┘
895 begin
st └─────
896 have : times_cont_diff 𝕜 n (λp : F, -p),
id └─────────────┘ ┴ ┴ ┴ ┴
src └─────┘└─────────────┘┴ ┴ ┴ └──┘ └┘┴ ┴
typ └─────┘└─────────────┘┴┴┴┴┴ └──┘┴└┘┴ ┴
doc └─────┘└─────────────┘┴ ┴ ┴ └──┘ └┘ ┴
txt └─────┘ ┴ ┴ ┴ └──┘ └┘ ┴
par └─────┘ ┴ ┴ ┴ └──┘ └┘ ┴
pid └───┘└┘ ┴ ┴ ┴ └──┘ └┘ ┴
st ────────────────────────────────────────┘└─
897 { apply is_bounded_linear_map.times_cont_diff,
id └───────────────────────────────────┘
src └────┘└───────────────────────────────────┘
typ └────┘└───────────────────────────────────┘
doc └────┘└───────────────────────────────────┘
txt └────┘
par └────┘
pid ┴
st ───┘└─────────────────────────────────────────┘└─
898 exact is_bounded_linear_map.neg is_bounded_linear_map.id },
id └───────────────────────┘ └──────────────────────┘
src └────┘└───────────────────────┘┴└──────────────────────┘┴
typ └────┘└───────────────────────┘┴└──────────────────────┘┴
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ────────────────────────────────────────────────────────────┘└┘└
899 exact this.comp hf
id └───────┘ └┘
src └────┘└───────┘┴ ┴
typ └────┘└───────┘┴└┘┴
doc └────┘└───────┘┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ────────────────────┘
900 end
st └─┘
901
902 /--
903 The difference of two C^n functions on a domain is C^n.
904 -/
905 lemma times_cont_diff_on.sub {n : with_top ℕ} {s : set E} {f g : E → F}
id └──────┘ ┴ └─┘ ┴ ┴ ┴
src └──────┘ ┴ └─┘
typ └──────┘ ┴ └─┘ ┴ ┴ ┴
906 (hf : times_cont_diff_on 𝕜 n f s) (hg : times_cont_diff_on 𝕜 n g s) (hs : unique_diff_on 𝕜 s) :
id └────────────────┘ ┴ ┴ ┴ ┴ └────────────────┘ ┴ ┴ ┴ ┴ └────────────┘ ┴ ┴
src └────────────────┘ └────────────────┘ └────────────┘
typ └────────────────┘ ┴ ┴ ┴ ┴ └────────────────┘ ┴ ┴ ┴ ┴ └────────────┘ ┴ ┴
doc └────────────────┘ └────────────────┘ └────────────┘
907 times_cont_diff_on 𝕜 n (λx, f x - g x) s :=
id └────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └────────────────┘ ┴
typ └────────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └────────────────┘
908 hf.add (hg.neg hs) hs
id └┘└──┘ └┘└──┘ └┘ └┘
src └──┘ └──┘
typ └┘└──┘ └┘└──┘ └┘ └┘
doc └──┘ └──┘
909
910 /--
911 The difference of two C^n functions is C^n.
912 -/
913 lemma times_cont_diff.sub {n : with_top ℕ} {f g : E → F}
id └──────┘ ┴ ┴ ┴
src └──────┘ ┴
typ └──────┘ ┴ ┴ ┴
914 (hf : times_cont_diff 𝕜 n f) (hg : times_cont_diff 𝕜 n g) :
id └─────────────┘ ┴ ┴ ┴ └─────────────┘ ┴ ┴ ┴
src └─────────────┘ └─────────────┘
typ └─────────────┘ ┴ ┴ ┴ └─────────────┘ ┴ ┴ ┴
doc └─────────────┘ └─────────────┘
915 times_cont_diff 𝕜 n (λx, f x - g x) :=
id └─────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─────────────┘ ┴
typ └─────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────────────┘
916 hf.add hg.neg
id └┘└──┘ └┘└──┘
src └──┘ └──┘
typ └┘└──┘ └┘└──┘
doc └──┘ └──┘